Automata-Based Confidentiality Monitoring
Automata-Based Confidentiality Monitoring
复制标题
基于自动机的机密性监控
DOI：
10.1007/978-3-540-77505-8_7
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
David A. Schmidt
中科院分区：
文献类型：
--
作者：
Gurvan Le Guernic;A. Banerjee;T. Jensen;David A. Schmidt
不干扰通常用作基线安全策略，以正式确定程序操纵的秘密信息的机密性。相对于非干扰的静态检查，本文考虑了动态的、基于自动化的、连续程序单次执行的信息流监控。监控机制是基于动态和静态分析的结合。在程序执行期间，程序事件的抽象被发送到自动机，自动机使用这些抽象来跟踪信息流，并通过禁止或编辑危险操作来控制执行。所提出的机制被证明是合理的，既能保证类型良好的程序的执行（在Volpano， Smith和Irvine的安全类型系统中），又能保证类型不良的程序的某些安全执行。
Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of non-interference, this paper considers dynamic, automaton-based, monitoring of information flow for a single execution of a sequential program. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. The mechanism proposed is proved to be sound, to preserve executions of well-typed programs (in the security type system of Volpano, Smith and Irvine), and to preserve some safe executions of ill-typed programs.