可信編譯構(gòu)造理論與關鍵技術

《信息科學技術學術著作叢書》序
前言

第1章 緒論
1.1 研究背景及意義
1.2 相關研究現(xiàn)狀
1.2.1 編譯器自身的安全性問題研究
1.2.2 編譯所生成程序代碼的安全性問題研究
1.2.3 安全程序設計語言及其相應編譯系統(tǒng)構(gòu)造方法研究
1.3 目標及內(nèi)容
1.3.1 編譯器自身的可信性研究
1.3.2 編譯所得可執(zhí)行代碼的可信性研究
1.4 本書組織結(jié)構(gòu)
1.5 本章小結(jié)
參考文獻

第2章 編譯器自身可信性
2.1 引言
2.2 可信編譯概念
2.3 編譯正確性證明
2.3.1 編譯器正確性
2.3.2 形式語義與語義保持
2.3.3 保證編譯器自身可信性方法
2.4 可信編譯器構(gòu)造
2.4.1 基于編譯器正確性的構(gòu)造方法
2.4.2 基于攜帶證明代碼的構(gòu)造方法
2.4.3 基于轉(zhuǎn)換檢驗的構(gòu)造方法
2.4.4 基于可證明微型編譯器的構(gòu)造方法
2.4.5 可信編譯器構(gòu)造方法對比分析
2.5 基于形式語義的編譯器正確性證明
2.5.1 源語言
2.5.2 目標語言
2.5.3 編譯轉(zhuǎn)換及正確性證明
2.6 編譯優(yōu)化正確性證明
2.6.1 中間語言語法和遷移系統(tǒng)
2.6.2 模擬關系及語義一致性驗證
2.6.3 編譯優(yōu)化實現(xiàn)正確性驗證過程
2.6.4 應用示例
2.6.5 結(jié)論
2.7 本章小結(jié)
參考文獻

第3章 編譯對象的可信性
3.1 引言
3.2 代碼可信性驗證機制
3.2.1 基于分離邏輯的程序驗證
3.2.2 基于模型檢測的程序驗證方法
3.3 代碼安全性加強機制
3.3.1 基于有色Petri網(wǎng)的緩沖區(qū)溢出檢測.NN
3.3.2 基于SMT求解器的程序驗證方法
3.4 可執(zhí)行代碼安全保護機制
3.4.1 基于壓縮的低開銷代碼保護策略
3.4.2 基于程序流敏感的自修改代碼混淆方法
3.4.3 程序動態(tài)完整性保護
3.5 本章小結(jié)
參考文獻

第4章 基于編譯嵌入式軟件優(yōu)化
4. 1引言
4.2 基于編譯的優(yōu)化框架
4.2.1 基于編譯的嵌入式系統(tǒng)優(yōu)化框架結(jié)構(gòu)設計
4.2.2 面向嵌入式平臺編譯優(yōu)化的中間語言設計
4.2.3 目標機器特征描述語言研究
4.3 傳統(tǒng)的編譯器優(yōu)化技術概述
4.3.1 機器無關的編譯器優(yōu)化技術
4.3.2 機器相關的編譯器優(yōu)化技術
4.4 內(nèi)存優(yōu)化
4.4.1 背景
4.4.2 分析
4.4.3 方法
4.4.4 一個例子
4.4.5 實驗結(jié)果
4.5 功耗優(yōu)化
4.5.1 功耗模型
4.5.2 基于編譯的功耗優(yōu)化方法
4.5.3 基于總線的功耗優(yōu)化實例
4.5.4 基于片上緩存的功耗優(yōu)化
4.6 本章小結(jié)
參考文獻

第5章 綠色編譯優(yōu)化
5.1 引言
5.2 綠色編譯器概念及優(yōu)化框架
5.2.1 綠色編譯器的概念
5.2.2 綠色編譯優(yōu)化框架
5.3 面向移動嵌入式系統(tǒng)的綠色編譯優(yōu)化方法研究
5.3.1 基于計算博弈論的混合存儲系統(tǒng)綠色編譯優(yōu)化
5.3.2 基于總線翻轉(zhuǎn)編碼和多維度集成學習的指令選擇和調(diào)度方法研究
5.3.3 基于編譯的多核環(huán)境下的并行程序綠色優(yōu)化
5.4 綠色評估模型
5.5 本章小結(jié)
參考文獻

第6章 基于編譯的軟件測試
6.1 引言
6.2 基于編譯的測試框架
6.3 測試需求描述語言
6.4 基于編譯的錯誤可跟蹤的自動測試方法
6.4.1 用于測試用例生成的擴展語法及對應語義
6.4.2 應用舉例
6.5 本章小結(jié)
參考文獻

第7章 基于編譯的可信軟件構(gòu)造及關鍵技術
7.1 引言
7.2 基于編譯的可信軟件開發(fā)過程模型
7.2.1 可信軟件開發(fā)過程模型
……
第8章 總結(jié)及展望