Page 134 - My FlipBook
P. 134
大
實驗
室
程式語言與形式方法實驗室
Research Laboratories 研究人員 程式語言與形式方法實驗室發展保證程式正確性之技術。我們在程式語言方面的研究，著
重於發展正確程式之語法、語意、及實務上之議題；在形式方法方面的研究，強調分析真
陳郁方 / 召集人 實程式中演算法、計算、以及實際方面之課題。我們應用數學及形式技術以探討我們的研
究問題，亦致力於發展工具及方法論以幫助程式開發者寫作正確程式。
研究員
一、函數程式語言驗證與推導
王柏堯
函數程式語言提供一個單純、多限制的計算模型，但相對地，我們也因此擁有數學的
研究員 好處：程式可當作數學來理解，可用包括歸納法在內的種種數學工具推論關於程式的
性質。可從一個簡單、好理解、但作為程式執行效率不高的程式開始，用數學方法推
柯向上 導出一個和它「相等」，但執行效率高的程式。這套技巧稱作「程式推導」。我們做
過幾個有趣的演算法推導，包括近似演算法、串列上的演算法等等。日後也將繼續尋
助研究員 找更多的程式推導例子，並建立推導程式的常用定理與步驟。
莊庭瑞 一般的印象是函數語言中不允許副作用的存在。事實上，許多實用的函數語言不僅支
援副作用，甚至支援許多種副作用。只是在函數語言中，我們會希望在支援副作用的
副研究員 同時不能失去函數語言原有的好處：副作用也須以嚴謹、能以數學方法管理的方式出
現在程式中。其中一種管理、描述副作用的方式是透過「單子」。我們近年來也研究
穆信成 如何證明單子程式的性質，並嘗試釐清確保多種副作用結合後仍保持其應有性質的充
分條件。
副研究員
二、依值型別編程
學界已有不少型別理論基礎和語言／系統根據「命題即型別」此一原則發展出來。在
這些系統中，證明數學定理就只是編寫具精巧型別（學名為「依值型別」）的程式。
其中較為大膽的一脈工作是依值型別編程，其目標是將完整的依值型別引入一般程式
語言內（特別是函式語言），不僅保證程式正確，同時還保留自然的編程風格。依值
型別編程的一大特徵是用迭構型別族系（最近亦能用迭解型別族系）將程式員關注的
性質編入型別內，程式員操作這些型別的構造與計算時便能不著痕跡地建立或利用型
別內嵌的性質，不需另寫證明，甚至能以型別資訊作為語意上的編程引導。我們已有
一些初步實驗顯示這個新範式能成功融合程式與證明，並將進一步探究其潛力。
三、低階密碼程式之正規驗證
現代密碼學仰賴大有限體上之計算。常見之計算設備卻不支援長整數（如：255 位元）
計算。因此，大有限體上之計算必須在 32 或是 64 計算結構上來實現。而這些實現必
然隨著計算結構不同而有所改變。在 OpenSSL 中，大有限體乘法已經有 x86、ARM、
SPARC 上之實現。這些組合程式是否正確地被實現，在密碼學之應用非常重要。我們
著重於發展實用的群與體運算密碼程式形式化驗證技術。藉由與密碼專家之合作，我
們的技術已經被用於驗證多種在 OpenSSL、Bitcoin、wolfSSL 中橢圖曲線密碼系統之群
與體運算。
132
實驗
室
程式語言與形式方法實驗室
Research Laboratories 研究人員 程式語言與形式方法實驗室發展保證程式正確性之技術。我們在程式語言方面的研究，著
重於發展正確程式之語法、語意、及實務上之議題；在形式方法方面的研究，強調分析真
陳郁方 / 召集人 實程式中演算法、計算、以及實際方面之課題。我們應用數學及形式技術以探討我們的研
究問題，亦致力於發展工具及方法論以幫助程式開發者寫作正確程式。
研究員
一、函數程式語言驗證與推導
王柏堯
函數程式語言提供一個單純、多限制的計算模型，但相對地，我們也因此擁有數學的
研究員 好處：程式可當作數學來理解，可用包括歸納法在內的種種數學工具推論關於程式的
性質。可從一個簡單、好理解、但作為程式執行效率不高的程式開始，用數學方法推
柯向上 導出一個和它「相等」，但執行效率高的程式。這套技巧稱作「程式推導」。我們做
過幾個有趣的演算法推導，包括近似演算法、串列上的演算法等等。日後也將繼續尋
助研究員 找更多的程式推導例子，並建立推導程式的常用定理與步驟。
莊庭瑞 一般的印象是函數語言中不允許副作用的存在。事實上，許多實用的函數語言不僅支
援副作用，甚至支援許多種副作用。只是在函數語言中，我們會希望在支援副作用的
副研究員 同時不能失去函數語言原有的好處：副作用也須以嚴謹、能以數學方法管理的方式出
現在程式中。其中一種管理、描述副作用的方式是透過「單子」。我們近年來也研究
穆信成 如何證明單子程式的性質，並嘗試釐清確保多種副作用結合後仍保持其應有性質的充
分條件。
副研究員
二、依值型別編程
學界已有不少型別理論基礎和語言／系統根據「命題即型別」此一原則發展出來。在
這些系統中，證明數學定理就只是編寫具精巧型別（學名為「依值型別」）的程式。
其中較為大膽的一脈工作是依值型別編程，其目標是將完整的依值型別引入一般程式
語言內（特別是函式語言），不僅保證程式正確，同時還保留自然的編程風格。依值
型別編程的一大特徵是用迭構型別族系（最近亦能用迭解型別族系）將程式員關注的
性質編入型別內，程式員操作這些型別的構造與計算時便能不著痕跡地建立或利用型
別內嵌的性質，不需另寫證明，甚至能以型別資訊作為語意上的編程引導。我們已有
一些初步實驗顯示這個新範式能成功融合程式與證明，並將進一步探究其潛力。
三、低階密碼程式之正規驗證
現代密碼學仰賴大有限體上之計算。常見之計算設備卻不支援長整數（如：255 位元）
計算。因此，大有限體上之計算必須在 32 或是 64 計算結構上來實現。而這些實現必
然隨著計算結構不同而有所改變。在 OpenSSL 中，大有限體乘法已經有 x86、ARM、
SPARC 上之實現。這些組合程式是否正確地被實現，在密碼學之應用非常重要。我們
著重於發展實用的群與體運算密碼程式形式化驗證技術。藉由與密碼專家之合作，我
們的技術已經被用於驗證多種在 OpenSSL、Bitcoin、wolfSSL 中橢圖曲線密碼系統之群
與體運算。
132
