计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2012年
5期
901-912
,共12页
孙聪%唐礼勇%陈钟%马建峰
孫聰%唐禮勇%陳鐘%馬建峰
손총%당례용%진종%마건봉
信息流%无干扰性%加权下推系统%自合成%可达性分析
信息流%無榦擾性%加權下推繫統%自閤成%可達性分析
신식류%무간우성%가권하추계통%자합성%가체성분석
信息流安全的形式化以无干扰性为标准属性.针对目前字节码级的信息流安全分析均未基于对程序无干扰性的语义表示,提出了一种基于语义的无干扰性自动验证方法.为适应语言特性和应用环境的限制,将基本自合成扩展为低安全级记录自合成,以支持对标错状态的可达性分析,保证标错状态不可达时对应字节码程序满足无干扰性.在此基础上为提高实际验证效率提出了3种模型优化方法.实验说明方法的可用性、效率、可扩展性及模型优化的实际效果.
信息流安全的形式化以無榦擾性為標準屬性.針對目前字節碼級的信息流安全分析均未基于對程序無榦擾性的語義錶示,提齣瞭一種基于語義的無榦擾性自動驗證方法.為適應語言特性和應用環境的限製,將基本自閤成擴展為低安全級記錄自閤成,以支持對標錯狀態的可達性分析,保證標錯狀態不可達時對應字節碼程序滿足無榦擾性.在此基礎上為提高實際驗證效率提齣瞭3種模型優化方法.實驗說明方法的可用性、效率、可擴展性及模型優化的實際效果.
신식류안전적형식화이무간우성위표준속성.침대목전자절마급적신식류안전분석균미기우대정서무간우성적어의표시,제출료일충기우어의적무간우성자동험증방법.위괄응어언특성화응용배경적한제,장기본자합성확전위저안전급기록자합성,이지지대표착상태적가체성분석,보증표착상태불가체시대응자절마정서만족무간우성.재차기출상위제고실제험증효솔제출료3충모형우화방법.실험설명방법적가용성、효솔、가확전성급모형우화적실제효과.
