软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2012年
8期
2149-2162
,共14页
信息流安全%机密消去%下推系统%自动验证%程序分析
信息流安全%機密消去%下推繫統%自動驗證%程序分析
신식류안전%궤밀소거%하추계통%자동험증%정서분석
针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效.
針對程序語言信息流安全領域的現有機密消去策略,提齣瞭一種基于下推繫統可達性分析的程序信息流安全驗證機製.將存儲-匹配操作內嵌于對抽象模型的緊湊自閤成結果中,使得對抽象結果中標錯狀態的可達性分析可以作為不同機密消去策略下程序安全性的驗證機製.實例研究說明,該方法比基于類型繫統的方法具有更高的精確性,且比已有的自動驗證方法更為高效.
침대정서어언신식류안전영역적현유궤밀소거책략,제출료일충기우하추계통가체성분석적정서신식류안전험증궤제.장존저-필배조작내감우대추상모형적긴주자합성결과중,사득대추상결과중표착상태적가체성분석가이작위불동궤밀소거책략하정서안전성적험증궤제.실례연구설명,해방법비기우류형계통적방법구유경고적정학성,차비이유적자동험증방법경위고효.
