计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2008年
3期
372-380
,共9页
陈意云%华保健%葛琳%王志芳
陳意雲%華保健%葛琳%王誌芳
진의운%화보건%갈림%왕지방
软件安全%指针逻辑%Hoare逻辑%指针分析%类型系统
軟件安全%指針邏輯%Hoare邏輯%指針分析%類型繫統
연건안전%지침라집%Hoare라집%지침분석%류형계통
在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.
在高可信軟件的各種性質中,安全性是被關註的重點,其中軟件滿足安全策略的證明方法是研究的熱點之一.文中根據作者所設想的安全程序的設計和證明框架,為類C語言的一箇子集設計瞭一箇指針邏輯繫統.該邏輯繫統是Hoare邏輯繫統的一種擴展,它用推理規則來錶達每一種語句引起指針信息的變化情況.它可用來對指針程序進行精確的指針分析,所穫得的信息用來證明指針程序是否滿足定型規則的附加條件,以支持程序的安全性驗證.該邏輯繫統也可用來證明指針程序的其它性質.
재고가신연건적각충성질중,안전성시피관주적중점,기중연건만족안전책략적증명방법시연구적열점지일.문중근거작자소설상적안전정서적설계화증명광가,위류C어언적일개자집설계료일개지침라집계통.해라집계통시Hoare라집계통적일충확전,타용추리규칙래표체매일충어구인기지침신식적변화정황.타가용래대지침정서진행정학적지침분석,소획득적신식용래증명지침정서시부만족정형규칙적부가조건,이지지정서적안전성험증.해라집계통야가용래증명지침정서적기타성질.
