On The Automated Synthesis Of Proof-Carrying Temporal Reference Monitors
LOPSTR'06 Proceedings of the 16th international conference on Logic-based program synthesis and transformation(2007)
摘要
We extend the range of security policies that can be guaranteed with proof carrying code from the classical type safety, control safety, memory safety, and space/time guarantees to more general security policies, such as general resource and access control. We do so by means of (1) a specification logic for security policies, which is the past-time fragment of LTL, and (2) a synthesis algorithm generating reference monitor code and accompanying proof objects from formulae of the specification logic. To evaluate the feasibility of our approach, we developed a prototype implementation producing proofs in Isabelle/HOL.
更多查看译文
关键词
security policy,specification logic,classical type safety,control safety,general security policy,memory safety,access control,accompanying proof object,general resource,monitor code,automated synthesis,temporal reference monitor
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要