1、一種安全語言的設(shè)計(jì)及形式證明華保健中國科學(xué)技術(shù)大學(xué)計(jì)算機(jī)系合作者：陳意云 李兆鵬 王志芳 葛 琳TexPoint fonts used in EMF. Read the TexPoint manual before you delete this box.: A軟件安全的挑戰(zhàn)軟件系統(tǒng)應(yīng)用越來越廣泛，其安全問題也愈發(fā)突出來源：CNCERT/CC 2006年度報(bào)告2007年上半年的統(tǒng)計(jì)數(shù)據(jù)已經(jīng)超過了06全年的統(tǒng)計(jì)數(shù)據(jù)程序設(shè)計(jì)語言本身的安全性對高安全需求軟件起著基礎(chǔ)作用現(xiàn)有研究方法及其問題（1）程序分析的方法基于這些方法的工具：LC-Lint、Purify和PREFix等相對簡單；可擴(kuò)展性好；代價(jià)相

2、對較低分析結(jié)果一般不具備完備性類型系統(tǒng)技術(shù)成功用于Java、C#和ML等廣泛使用的語言輕量級語法方法；模塊性良好表達(dá)能力有限；不允許顯式存儲管理現(xiàn)有研究方法及其問題（2）類型細(xì)化依賴類型、應(yīng)用類型和單元素類型等從不同層面一步增強(qiáng)了類型系統(tǒng)的表達(dá)能力受表達(dá)能力限制，僅在不多的論域取得了結(jié)果程序驗(yàn)證和公理語義攜帶證明的代碼（PCC）、ESC/Java和Spec#等更通用的框架；表達(dá)能力更強(qiáng)程序員負(fù)擔(dān)重；受限于定理證明器的證明能力我們的研究目標(biāo)安全語言設(shè)計(jì)和實(shí)現(xiàn)安全語言面向系統(tǒng)程序設(shè)計(jì)研究內(nèi)容語言設(shè)計(jì)；公理語義系統(tǒng)；出具證明編譯器；語言和公理系統(tǒng)的性質(zhì)證明等把攜帶證明的代碼技術(shù)（PCC）推向?qū)嵱妹嫦?/p>

3、系統(tǒng)程序設(shè)計(jì)語言；更豐富的安全策略對高安全需求軟件的設(shè)計(jì)和實(shí)現(xiàn)技術(shù)進(jìn)行探索依靠程序設(shè)計(jì)語言設(shè)計(jì)和實(shí)現(xiàn)技術(shù)本文主要工作和貢獻(xiàn)研究了類型系統(tǒng)和邏輯系統(tǒng)相結(jié)合的安全機(jī)制應(yīng)用到所設(shè)計(jì)的類C的命令式語言PointerC上主要特色是定型規(guī)則中包含顯式副條件副條件表達(dá)更豐富的安全策略提出了指針邏輯Hoare邏輯的擴(kuò)展證明了語言的安全性和指針邏輯的可靠性用機(jī)械化方法證明在Coq中完成源語言PointerC源語言PointerC是類C的命令式語言選取了C語言核心的表達(dá)式和控制結(jié)構(gòu)包含malloc，free操作為什么選擇C？C是最重要的系統(tǒng)程序設(shè)計(jì)語言之一，但不安全出于效率考慮使用類型系統(tǒng)和邏輯系統(tǒng)相結(jié)合的靜態(tài)機(jī)

4、制研究重點(diǎn)是指針操作的安全問題類型系統(tǒng)、副條件PointerC定型規(guī)則包含顯式的副條件典型示例：斷言語言擴(kuò)展的一階邏輯必須證明這些副條件 成立保證程序的安全性指針邏輯的設(shè)計(jì)目的證明副條件成立是困難的副條件和值相關(guān)傳統(tǒng)上依賴運(yùn)行時(shí)動態(tài)檢查不成立則拋出異常Java/C#等試圖靜態(tài)證明副條件以Hoare邏輯推理的方式困難部分是指針操作的安全性對Hoare邏輯做了擴(kuò)展，提出指針邏輯指針邏輯（1）基本思想在每個(gè)程序點(diǎn)表達(dá)指針值的信息有效、空或者懸空p = malloc ();指針邏輯（2）基本思想在每個(gè)程序點(diǎn)表達(dá)指針值的信息有效、空或者懸空p, q / p-nextp = malloc ();邏輯命題n

5、extpq指針邏輯（3）基本思想以推理規(guī)則表達(dá)語句給指針信息帶來的變化最強(qiáng)后條件演算p, q / p-nextp = malloc ();前條件nextpq指針邏輯（4）基本思想以推理規(guī)則表達(dá)語句給指針信息帶來的變化最強(qiáng)后條件演算p, q / p-nextp = malloc ();p / q / q-next/ p-nextD前條件nextpq后條件qnextnextp操作語義操作語義的定義基于抽象機(jī)器模型包括全局變量區(qū)、棧、堆等操作語義由一系列歸約規(guī)則組成語句 在機(jī)器模型 上的執(zhí)行在機(jī)器模型上形式描述安全策略：無下標(biāo)越界無空（懸空）指針引用無內(nèi)存泄漏語言安全性定理及其證明經(jīng)過類型系統(tǒng)和指針

6、邏輯檢查的程序是安全的不違反安全策略證明步驟：機(jī)器模型上形式化安全策略無數(shù)組越界，無空（懸空）指針引用；無內(nèi)存泄漏證明安全策略對操作語義是不變式（Invariant）證明在Coq中完成機(jī)械化證明 語言語法操作語義類型系統(tǒng)安全性證明機(jī)械化的元邏輯 (CiC)TCB指針邏輯可靠性定理及其證明證明指針邏輯（公理語義系統(tǒng)）對PointerC的操作語義可靠。主要步驟：給出指針邏輯斷言在機(jī)器模型上的語義解釋特別考慮了推理規(guī)則中的副條件在基礎(chǔ)邏輯中形式化指針邏輯的推理規(guī)則包括斷言證明指針邏輯對操作語義可靠如果一個(gè)斷言在語法系統(tǒng)中可證，則它語義有效證明在Coq中完成機(jī)械化證明 語言語法操作語義類型系統(tǒng)安全性證

7、明機(jī)械化的元邏輯 (CiC)TCB斷言語言指針邏輯可靠性證明出具證明編譯器PLCC 源程序 + 源級規(guī)范標(biāo)注驗(yàn)證條件生成器定理證明器驗(yàn)證條件代碼和規(guī)范的生成證明生成驗(yàn)證條件的證明匯編代碼 + 規(guī)范匯編代碼 + 規(guī)范 + 證明出具證明的編譯器證明檢查器相關(guān)工作程序性質(zhì)證明ESC，ATS等面向系統(tǒng)編程的安全語言Cyclone，CCured等出具證明的編譯器Flint/SML, TouchStone, Special J, TIL/TAL等語言定義和實(shí)現(xiàn)的機(jī)械化SML（Twelf），CMinor（Coq），CAP（Coq）等進(jìn)一步的工作擴(kuò)展源語言支持部分指針?biāo)阈g(shù)calloc操作擴(kuò)展指針邏輯系統(tǒng)支持不

8、規(guī)則數(shù)據(jù)結(jié)構(gòu)的推理，如圖等設(shè)計(jì)和實(shí)現(xiàn)出具證明編譯器原型系統(tǒng)研究編譯器和定理證明器交互程序驗(yàn)證和程序優(yōu)化等結(jié)論研究了類型系統(tǒng)和邏輯系統(tǒng)相結(jié)合的安全機(jī)制應(yīng)用到所設(shè)計(jì)的類C的命令式語言PointerC上主要特色是定型規(guī)則中包含顯式副條件副條件表達(dá)更豐富的安全策略提出了指針邏輯Hoare邏輯的擴(kuò)展證明了語言的安全性和指針邏輯的可靠性用機(jī)械化方法證明在Coq中完成了解更多歡迎訪問軟件安全實(shí)驗(yàn)室主頁，了解更多信息http:/謝謝！附加的幻燈片附加的幻燈片指針邏輯設(shè)計(jì)了指針邏輯靜態(tài)推理證明這些邏輯命題基于Hoare邏輯的公理語義系統(tǒng)核心思想以邏輯命題精確表達(dá)在每個(gè)程序點(diǎn)的有效指針、空指針和懸空指針的信息設(shè)計(jì)

9、推理規(guī)則來推理程序語句給這些指針信息帶來的變化斷言語言基于一階邏輯演算規(guī)則類似于Hoare邏輯系統(tǒng)的最強(qiáng)后條件演算指針邏輯可靠性定理及其證明證明指針邏輯（公理語義系統(tǒng)）對PointerC的操作語義可靠。主要步驟：給出斷言 在機(jī)器模型上的語義解釋特別考慮了推理規(guī)則中的副條件指針邏輯對操作語義可靠證明在Coq中完成語言安全性定理及其證明經(jīng)過類型系統(tǒng)和指針邏輯檢查的程序是安全的不違反安全策略證明步驟：在機(jī)器模型上形式化安全策略無數(shù)組越界，無空（懸空）指針引用；無內(nèi)存泄漏證明安全策略對操作語義是不變式（Invariant）證明在Coq中完成和PCC相比較的優(yōu)勢？從可生成攜帶證明的代碼的角度來說，本工作進(jìn)一步把PCC技術(shù)推向?qū)嵱玫辽僭谝韵聨c(diǎn)，存在顯著不同源語言的靈活性安全策略的豐富程度出具證明編譯器所能支持Hoare邏輯風(fēng)格推理的支持程度PointerC對Java或者M(jìn)L等類型安全的語言的優(yōu)勢？