匯編指針程序安全性驗證的研究.pdf

1、中國科學技術大學博士學位論文匯編指針程序安全性驗證的研究姓名：李兆鵬申請學位級別：博士專業(yè)：計算機軟件與理論指導教師：陳意云20080401摘要證明等方面的研究，然后介紹了本項目組提出的一個使用指針邏輯的安全軟件開發(fā)和驗證框架?；谠摽蚣芟拢疚闹亟榻B匯編程序一級的驗證框架的設計和實現(xiàn)。本文提出了匯編級指針邏輯來對匯編指針程序安全性質的進行驗證。本文還實現(xiàn)了一個原型系統(tǒng)，并使用該系統(tǒng)對鏈表、二叉樹等非平凡的指針程序的進行了自動的安全驗

2、證。本文的主要特色和貢獻為：設計了一種基于x86機器模型、Hoare邏輯風格的形式證明框架，豐富了出具證明編譯器的目標級基礎研究。設計了一種用于匯編指針程序安全性證明的指針邏輯，解決了Hoare邏輯處理別名面臨的困難，使得拓展后的指針邏輯成為匯編程序性質證明的一種新工具。證明了匯編語言指針邏輯的可靠性。并己在證明輔助工具Coq中完成。實現(xiàn)了一個匯編級驗證原型系統(tǒng)。本文使用該系統(tǒng)對鏈表、二叉樹等非平凡的指針程序的進行了自動的安全驗證。本工