摘要
嵌入监控代码方法一般是在原程序中嵌入监控代码后生成自监控软件,实现安全策略对软件行为的约束,受自监控软件实现方式等具体研究方法限制,目前验证自监控软件行为符合目标安全策略的方法验证能力有限。提出一种灵活的基于面向方面编程的自监控软件实现方式,并设计了相应更全面的自监控软件行为正确性验证方法。该方法基于交替转换系统描述自监控软件的行为,使用时间交替时序逻辑定义软件行为正确的性质公式,通过给定算法在模型上检测性质公式满足与否,从而验证软件行为是否符合"安全性"、"活性"等类型监控策略,并可以分析监控代码对原程序的影响。
The embedded monitoring code method commonly embeds monitoring codes into the original program to create the self-monitoring program,thus realizing the restriction of software behaviors by the security policy.Due to limitations of detailed researching methods such as the self-monitoring program implementation methods,the ability of the method to verify whether the self-monitoring program behavior complies with the objective security policy is confined.A swift aspect-oriented programming based self-monitoring program implementation method is proposed.Moreover a corresponding and more all-rounded self-monitoring program behavior correctness verification method is designed,detailedly,to base on the alternating transition system to describe the self-monitoring program behavior,to use time alternating temporal logic to define program behavior correctness natural formula,and to use the specified algorithm to detect on the model whether the natural formula is satisfactory or not to verify whether the program behavior complies with monitoring policies such as security,liveliness and so forth,and at last to be able to analyze the influence of the monitoring code on the original program.
出处
《计算机应用与软件》
CSCD
北大核心
2012年第3期202-205,231,共5页
Computer Applications and Software
关键词
自监控软件
面向方面
交替转换系统
时间交替时序逻辑
Self-monitoring program Aspect-oriented Alternating transition system Time alternating temporal logic
