计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2008年
4期
556-564
,共9页
华保健%陈意云%李兆鹏%王志芳%葛琳
華保健%陳意雲%李兆鵬%王誌芳%葛琳
화보건%진의운%리조붕%왕지방%갈림
软件安全%语言设计%类型系统%Hoare逻辑%指针逻辑
軟件安全%語言設計%類型繫統%Hoare邏輯%指針邏輯
연건안전%어언설계%류형계통%Hoare라집%지침라집
程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的.
程序設計語言本身的安全性在高安全需求軟件的設計和實現中起著基礎作用.該文在用于繫統級編程的安全語言的設計和性質證明方麵,做瞭有益的嘗試.作者設計瞭一箇類C的命令式語言PointerC,其主要特點在于其類型繫統中包含顯式的副條件(side conditions),這些副條件本質上是約束程序語法錶達式值的邏輯公式.該文證明瞭PointerC語言的安全性定理,即滿足這些副條件的程序,在執行時不會違反語言的安全策略.為靜態推理副條件中涉及指針的命題,作者已經提齣瞭一種指針邏輯(pointer logic),文中證明瞭指針邏輯對操作語義是可靠的.
정서설계어언본신적안전성재고안전수구연건적설계화실현중기착기출작용.해문재용우계통급편정적안전어언적설계화성질증명방면,주료유익적상시.작자설계료일개류C적명령식어언PointerC,기주요특점재우기류형계통중포함현식적부조건(side conditions),저사부조건본질상시약속정서어법표체식치적라집공식.해문증명료PointerC어언적안전성정리,즉만족저사부조건적정서,재집행시불회위반어언적안전책략.위정태추리부조건중섭급지침적명제,작자이경제출료일충지침라집(pointer logic),문중증명료지침라집대조작어의시가고적.
