计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2008年
5期
825-833
,共9页
李兆鹏%陈意云%葛琳%华保健
李兆鵬%陳意雲%葛琳%華保健
리조붕%진의운%갈림%화보건
软件安全%出具证明编译器%指针逻辑%Hoare逻辑%携带证明的汇编程序
軟件安全%齣具證明編譯器%指針邏輯%Hoare邏輯%攜帶證明的彙編程序
연건안전%출구증명편역기%지침라집%Hoare라집%휴대증명적회편정서
在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查.
在高可信軟件的各種性質中,安全性是關註的重點.軟件滿足安全策略的證明方法是安全性研究的熱點之一.根據前期提齣的安全程序設計與證明的框架以及指針邏輯推理繫統,介紹在所實現的齣具證明編譯器(certifying compiler)原型繫統中有關目標機器的形式定義、彙編程序的形式驗證框架以及彙編程序指針程序性質證明等方麵的研究.它們的主要特點是彙編驗證框架是基于Hoare風格的程序驗證方式;與指針有關的性質使用和源語言一級類似的指針邏輯推理繫統進行證明;使用一箇簡單的類型繫統完成有關指針的類型檢查.
재고가신연건적각충성질중,안전성시관주적중점.연건만족안전책략적증명방법시안전성연구적열점지일.근거전기제출적안전정서설계여증명적광가이급지침라집추리계통,개소재소실현적출구증명편역기(certifying compiler)원형계통중유관목표궤기적형식정의、회편정서적형식험증광가이급회편정서지침정서성질증명등방면적연구.타문적주요특점시회편험증광가시기우Hoare풍격적정서험증방식;여지침유관적성질사용화원어언일급유사적지침라집추리계통진행증명;사용일개간단적류형계통완성유관지침적류형검사.
