小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2011年
6期
1164-1169
,共6页
张臻婷%李兆鹏%陈意云%杨思敏%庄重
張臻婷%李兆鵬%陳意雲%楊思敏%莊重
장진정%리조붕%진의운%양사민%장중
程序验证%携带证明代码%出具证明编译器%汇编级验证
程序驗證%攜帶證明代碼%齣具證明編譯器%彙編級驗證
정서험증%휴대증명대마%출구증명편역기%회편급험증
携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查证明,从而保证汇编代码的安全性.本文设计了一种Hoare风格的汇编级验证框架,并在此框架下提出并实现一种新的自动生成汇编级断言和证明的方法.
攜帶證明代碼允許代碼消費方通過檢查代碼生產方提供的證明,來判斷代碼是否滿足相應的安全規範.本文實現瞭一箇類C語言的齣具證明編譯器原型,它在將帶有規範標註的源代碼編譯成彙編代碼的同時,還能產生彙編代碼滿足相應規範的Coq可檢查證明,從而保證彙編代碼的安全性.本文設計瞭一種Hoare風格的彙編級驗證框架,併在此框架下提齣併實現一種新的自動生成彙編級斷言和證明的方法.
휴대증명대마윤허대마소비방통과검사대마생산방제공적증명,래판단대마시부만족상응적안전규범.본문실현료일개류C어언적출구증명편역기원형,타재장대유규범표주적원대마편역성회편대마적동시,환능산생회편대마만족상응규범적Coq가검사증명,종이보증회편대마적안전성.본문설계료일충Hoare풍격적회편급험증광가,병재차광가하제출병실현일충신적자동생성회편급단언화증명적방법.
