匯編指針程序安全性驗(yàn)證的研究.pdf

1、中國(guó)科學(xué)技術(shù)大學(xué)博士學(xué)位論文匯編指針程序安全性驗(yàn)證的研究姓名：李兆鵬申請(qǐng)學(xué)位級(jí)別：博士專業(yè)：計(jì)算機(jī)軟件與理論指導(dǎo)教師：陳意云20080401摘要證明等方面的研究，然后介紹了本項(xiàng)目組提出的一個(gè)使用指針邏輯的安全軟件開發(fā)和驗(yàn)證框架。基于該框架下，本文著重介紹匯編程序一級(jí)的驗(yàn)證框架的設(shè)計(jì)和實(shí)現(xiàn)。本文提出了匯編級(jí)指針邏輯來(lái)對(duì)匯編指針程序安全性質(zhì)的進(jìn)行驗(yàn)證。本文還實(shí)現(xiàn)了一個(gè)原型系統(tǒng)，并使用該系統(tǒng)對(duì)鏈表、二叉樹等非平凡的指針程序的進(jìn)行了自動(dòng)的安全驗(yàn)

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