?前言：當前，復雜而泛在的軟體架構支撐著全球經濟，編譯器和計算機高級語言正是這些軟體的基石，編譯器作為產生代碼的工具，在加強計算機安全方面扮演著至關重要的角色，對于安全關鍵領域的系統軟體而言，必須考慮編譯器引入的錯誤，否則高成本的源程式級驗證作業可能在目標程式級失效[1]，
保證編譯器正確性的傳統方法是進行大量的測驗，但測驗用例覆寫范圍的不完全性使得編譯器中的錯誤可能被遺漏，且無法保證編譯器自身的正確性，對編譯器的正確性進行驗證是解決問題的根本途徑，其中最為嚴格的驗證手段莫過于采用形式化方法，經過形式化驗證的CompCert?編譯器正是可信編譯器的杰出代表，
CompCert可用于編譯“生命關鍵型”和“任務關鍵型”軟體，幾乎完全支持ISO?C 2011，ISO?C 1999和ANSI?C語言標準，支持PowerPC、ARM、x86和RISC-V架構，性能優于GCC(-O1），
CompCert編譯器的源語言為CompCert C，是C語言的大子集（幾乎是完整的ISO C99），與其他編譯器的不同之處在于，CompCert編譯器通過機器輔助的數學證明，驗證了自身不存在誤編譯問題，換句話說，其產生的可執行代碼與C語言原始碼語意指定的行為完全一致，
使用CompCert編譯器是對在源代碼級應用形式化驗證技術（靜態分析、程式證明、模型檢查等）的自然補充：CompCert編譯器的正確性證明保證了所生成的可執行代碼同樣具備源代碼上驗證的所有安全屬性，
01.你的編譯器可信嗎？
通常來講，編譯器是實作精細演算法的復雜軟體，確實可能存在bug，并可能導致一個正確的源程式中悄無聲息地生成錯誤可執行代碼，換句話說，一個有bug的編譯器可能在其所編譯的程式中插入bug——這種現象被稱為“誤編譯”，
一些實證研究表明，許多編譯器都存在誤編譯問題，1995年Nullstone ?C一致性測驗套件官網中就曾提到：
2005年學者E. Eide和J. Regehr的報告中也曾提及C編譯器出現的類似問題——易失性記憶體訪問：
2011年的《Finding and understanding bugs in C compilers》對C編譯器的測驗情況進行了總結，再次發現了許多誤編譯問題：
對于非安全關鍵的“日常”軟體來說，誤編譯可能不算是大問題：與源程式中已存在的錯誤相比，編譯器引入的錯誤可以忽略不計，然而，對于安全關鍵型軟體來說，情況則大不相同：此類軟體往往與生命安全、關鍵基礎設施或高敏資訊息息相關，如存在誤編譯問題則可能導致難以承擔的后果，必須通過復雜且成本高昂的驗證作業來解決——例如對生成的匯編碼進行額外的測驗和代碼審查，
除了安全問題外，誤編譯還會削弱使用工具對源程式進行輔助驗證的有效性，越來越多軟體的開發程序開始使用到如靜態分析工具和模型?檢查工具等形式化驗證工具，盡管高級的驗證工具能夠自動建立有價值的程式安全屬性（如無陣列訪問越界問題、無算術溢位等運行時錯誤），但這些工具大多是在C?語言源代碼上運行的，一個存在bug的編譯器可能使原始碼級形式化驗證提供的安全保障失效，產生不正確的可執行檔案，從而導致經過形式化驗證的源程式崩潰或出現錯誤，
02.編譯器的形式化驗證
CompCert專案為誤編譯問題提出了一個基于數學的根本性解決方案：對編譯器本身進行形式化、經工具輔助的驗證，通過對編譯器的源代碼應用程式證明技術，可以用數學層面的確定性證明編譯器產生的可執行代碼的行為完全符合?C?語言源程式的語意規定，從而排除所有誤編譯的風險，
歷史上對編譯器進行驗證的探索早已開始：第一個編譯器正確性證明（用于將算術運算式轉換為堆疊機）發布于1967年，自那時起，編譯器驗證便一直是許多學術研究的主題，CompCert專案一直致力于提供一個用于生產安全關鍵領域嵌入式系統軟體的完整、可實作的、經過優化的編譯器，
1.語意保持?
CompCert的形式化驗證包括證明以下定理：
對于所有源程式S 和編譯器生成的代碼C?，如編譯器應用于源程式S ，產生代碼C且未報告編譯錯誤，則C的可觀察行為（observable behaviors）就翻譯了一個?S 允許的可觀察行為，即“語意保持”，
2.什么是可觀察行為？
簡而言之，可觀察行為包括程式的用戶或其執行所在的物理世界能“看到”的關于程式行為的一切（除執行時間和記憶體消耗之外），更準確地說，CompCert遵循的是ISO ?C標準，具體可見下列應用CompCert時出現的情況：
程式存在終止、執行兩種狀態：終止狀態有正常終止（從主函式回傳）、錯誤終止（遇到未定義行為，如整數除以0），
所有對執行輸入/輸出的標準庫函式的呼叫，如printf()或getchar()，
所有對volatile全域變數的讀寫訪問，這些變數應用于記憶體映射的硬體設備，因此對其的任何讀/寫都被視為輸入/輸出操作，
因此，程式的可觀察行為是對其所執行的所有輸入/輸出和易失性操作的跟蹤，和其是否終止及如何終止（正常或發生錯誤時）的指示，
3.關于原始碼級驗證，語意保持告訴了我們什么？
語意保持定理的一個簡單推論如下：
- 假設Σ是一組可接受行為，表征了程式所需的安全或活性；
- 假設源程式S滿足Σ：S所有可能的可觀察行為都在Σ中；
- 進一步假設編譯器應用于源程式S，生成代碼C；
- 編譯后的代碼C滿足Σ：C的可觀察行為都在Σ中，
可靠的原始碼級驗證工具的目的在于建立一個規范Σ（對源程式S所有可能的執行都適用），這個規范可以由用戶定義，例如作為前置條件和后置條件；或者由工具確定，例如不存在運行時錯誤，因此，一個經過形式化驗證的編譯器能夠保證：如果一個可靠的原始碼級驗證工具確認程式滿足所用規范，那么真正執行的編譯代碼也滿足這個規范，
換句話說，只要在源程式上建立的“保證”延續到最后實際執行的編譯代碼，使用經過形式化驗證的編譯器就可以證明對原始碼級的驗證是正確的，
4.如何進行語意保持的證明？
由于優化編譯器固有的復雜性，其語意保持的證明是一項重大作業：
將其分成15個獨立的語意保持證明，每一個都在CompCert編譯器中進行驗證，最終的語意保持定理來自這些單獨證明的組合，對于每一次遍歷，必須證明對【所有可能的輸入程式】和【輸入程式所有可能的執行】都保持語意不變（根據輸入操作的不可預測結果，可能存在許多這樣的執行），
為此，需要考慮程式執行程序中每一個可能的可達狀態，以及形式語義下該狀態可執行的每一個轉換，語意保持的證明利用了編程語言的歸納結構：例如，為證明復合運算式a?+b被正確編譯，通過歸納假設，假定兩個較小的子運算式?a和?b被正確編譯，然后將這些結果基于“+”運算子相結合，
以上程序如果用紙筆來進行編譯證明，可能要寫幾百頁——極少有數學家愿意進行驗證，而現今可以利用計算機的強大功能：CompCert最突出的特點就是其大部分實作是在證明輔助器Coq環境中完成的，并且除詞法分析和某些預處理程序外，各個翻譯階段均在Coq中實作了正確性證明[1]，
5.形式化編譯器驗證的有效性如何？
?CompCert作業目前仍在進行中，還未實作完整的、端到端的形式化驗證：目前，約90%的編譯器演算法（包括所有優化和代碼生成演算法）已在Coq中被證明是正確的，但其余10%（包括精化、預處理、匯編和鏈接）還未得到驗證，將在未來得到改善，盡管如此，與普通編譯器相比，這種不完全的形式化驗證已經顯示出了正確性上的重大改進，《Finding and understanding bugs in C compilers》中提到：
?▲CompCert?編譯器架構
03.CompCert?在實踐中的應用
1.CompCert?提供下列架構的代碼生成器
- 32位和64位的PowerPC；
- 32位ARM v6、v7和v8，帶VFP協處理器；
- 64位ARM v8（AArch64架構）；
- 32位和64位的x86（IA32/AMD64），在32位模式下需要SSE2擴展；
- 32位和64位的RISC-V，分別采用ILP32D和LP64D的呼叫約定，
注：CompCert在某些情況下可能會使用浮點暫存器，除非指定選項-fno-fpu，
每個架構支持的應用二進制介面（ABI）和作業系統情況如下：?
2.CompCert?具備良好的代碼生成性能
▲在Power7處理器上CompCert與GCC 4.1.2生成的代碼性能比較
注：線條越短代表性能越強，基線(藍色)為未經優化的GCC，紅色為CompCert，
04.總結
近年來，有關編譯器形式化驗證的研究作業已取得長足的進步，達到了實用化水平，為未來制定新的工業標準奠定了強有力的基礎，CompCert編譯器作為經過形式化驗證的可信編譯器杰出代表，達到了人們所能期望的最高可信程度，關于Csmith的研究作業表明：CompCert在正確性方面的表現明顯優于常用的開源或商用C語言編譯器，
L2C可信編譯器的開發始于2010年9月，采用類似于CompCert編譯器的方法，以擴展的Lustre語言作為源語言, 以CompCert的Clight作為目標語言, 驗證方面與CompCert完全對接，
建模仿真與代碼生成軟體ModelCoder采用L2C可信編譯器，支持基于模型的嵌入式系統設計、仿真與可信代碼自動生成，用戶在開發早期便可基于虛擬模型進行持續測驗和驗證，適用于無線通信、電力電子、控制系統、信號處理等領域，
參考鏈接
[1] 楊萍,王生原. CompCert編譯器目標代碼生成機制分析[J]. 計算機科學, 2020, 47(9):7.
[2] https://compcert.org/man/manual001.html
[3] https://blog.csdn.net/xsx_6361/article/details/117519601
?轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/548828.html
標籤：其他