Page 36 - 2017 Brochure
P. 36
究群
程式語言與形式方法實驗室
程式語言與形式方法實驗室發展保證程式正確性之技術。 碼專家之合作，我們的技術已經被用於驗證安全橢圓曲線
我們在程式語言方面的研究，著重於發展正確程式之語法、 Curve25519 群運算中的 Montegory Ladderstep。
語意、及實務上之議題；在形式方法方面的研究，強調分
析真實程式中演算法、計算、以及實際方面之課題。我們 (3) 函數程式語言驗證與推導
應用數學及形式技術以探討我們的研究問題，亦致力於發
展工具及方法論以幫助程式開發者寫作正確程式。 函數程式語言提供一個單純、多限制的計算模型，但相對
地，我們也因此擁有數學的好處：程式可當作數學來理解，
(1) MapReduce 程式的自動驗證與生成 可用包括歸納法在內的種種數學工具推論關於程式的性質。
可從一個簡單、好理解、但作為程式執行效率不高的程式
MapReduce 是很流行的資料平行運算模型。在 MapReduce 開始，用數學方法推導出一個和它「相等」，但執行效率
中，reducer 讀取一個串列的資料並產生對應的輸出。由於 高的程式。這套技巧稱作「程式推導」。我們做過幾個有
各平台排程策略不同，reducer 的輸入可能在每次執行時以 趣的演算法推導，包括近似演算法、串列上的演算法等等。
不同順序抵達，因而產生了「reducer 可交換性問題」： 日後也將繼續尋找更多的程式推導例子，並建立推導程式
reducer 的輸出和輸入到達的順序是否無關？我們證明了此 的常用定理與步驟。
問題在輸入的資料為數學整數時，是無法被決定的。然而，
當輸入的資料型態為有限整數 ( 例如，電腦中的 64 位元整 一般的印象是函數語言中不允許副作用的存在。事實上，
數 ) 時，此問題是可被決定的。我們開發了名為「有理數暫 許多實用的函數語言不僅支援副作用，甚至支援許多種副
存器自動機」的模型來表述 reducer 程式。該模型有許多良 作用。只是在函數語言中，我們會希望在支援副作用的同
好的數學性質，例如，相等和可交換性問題可在多項式空
間內被解答。我們計劃以此模型作為 reducer 程式自動生成
的基礎。
(2) 低階密碼程式之正規驗證
現代密碼學仰賴大有限體上之計算。常見之計算設備卻不
支援長整數（如 255 位元）計算。因此，大有限體上之計
算必須藉由 32 或是 64 位元指令來實現，而這些實現必然
隨著計算結構不同而有所改變。在 OpenSSL 中，大有限
體乘法已經有 x86、ARM、SPARC 上之實現。這些低階組
合程式是否正確地被實現，在密碼學上非常重要。我們著
重於發展實用的低階密碼程式形式化驗證技術。藉由與密
34 研究群 Research Laboratories
程式語言與形式方法實驗室
程式語言與形式方法實驗室發展保證程式正確性之技術。 碼專家之合作，我們的技術已經被用於驗證安全橢圓曲線
我們在程式語言方面的研究，著重於發展正確程式之語法、 Curve25519 群運算中的 Montegory Ladderstep。
語意、及實務上之議題；在形式方法方面的研究，強調分
析真實程式中演算法、計算、以及實際方面之課題。我們 (3) 函數程式語言驗證與推導
應用數學及形式技術以探討我們的研究問題，亦致力於發
展工具及方法論以幫助程式開發者寫作正確程式。 函數程式語言提供一個單純、多限制的計算模型，但相對
地，我們也因此擁有數學的好處：程式可當作數學來理解，
(1) MapReduce 程式的自動驗證與生成 可用包括歸納法在內的種種數學工具推論關於程式的性質。
可從一個簡單、好理解、但作為程式執行效率不高的程式
MapReduce 是很流行的資料平行運算模型。在 MapReduce 開始，用數學方法推導出一個和它「相等」，但執行效率
中，reducer 讀取一個串列的資料並產生對應的輸出。由於 高的程式。這套技巧稱作「程式推導」。我們做過幾個有
各平台排程策略不同，reducer 的輸入可能在每次執行時以 趣的演算法推導，包括近似演算法、串列上的演算法等等。
不同順序抵達，因而產生了「reducer 可交換性問題」： 日後也將繼續尋找更多的程式推導例子，並建立推導程式
reducer 的輸出和輸入到達的順序是否無關？我們證明了此 的常用定理與步驟。
問題在輸入的資料為數學整數時，是無法被決定的。然而，
當輸入的資料型態為有限整數 ( 例如，電腦中的 64 位元整 一般的印象是函數語言中不允許副作用的存在。事實上，
數 ) 時，此問題是可被決定的。我們開發了名為「有理數暫 許多實用的函數語言不僅支援副作用，甚至支援許多種副
存器自動機」的模型來表述 reducer 程式。該模型有許多良 作用。只是在函數語言中，我們會希望在支援副作用的同
好的數學性質，例如，相等和可交換性問題可在多項式空
間內被解答。我們計劃以此模型作為 reducer 程式自動生成
的基礎。
(2) 低階密碼程式之正規驗證
現代密碼學仰賴大有限體上之計算。常見之計算設備卻不
支援長整數（如 255 位元）計算。因此，大有限體上之計
算必須藉由 32 或是 64 位元指令來實現，而這些實現必然
隨著計算結構不同而有所改變。在 OpenSSL 中，大有限
體乘法已經有 x86、ARM、SPARC 上之實現。這些低階組
合程式是否正確地被實現，在密碼學上非常重要。我們著
重於發展實用的低階密碼程式形式化驗證技術。藉由與密
34 研究群 Research Laboratories
