Proving Noninterference and Functional Correctness Using Traces
Proving Noninterference and Functional Correctness Using Traces
复制标题
使用迹线证明无干扰和功能正确性
DOI：
10.3233/jcs-1992-1103
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
J. McLean
中科院分区：
文献类型：
--
作者：
J. McLean
软件规范的跟踪方法被扩展为过程编程语言提供自然语义。此扩展提供了一种证明程序正确性的方法，该方法允许直接证明程序无干扰，而无需生成中间有限状态机和展开条件。这种方法为推理抽象软件系统规范及其实现提供了一个统一的框架。它还允许我们在抽象级别证明安全性，以便对不影响功能行为的程序进行更改不会影响安全性证明。
The trace method of software specification is extended to provide a natural semantics for a procedural programming language. This extension provides a method for proving program correctness that permits a direct proof of program Noninterference without having to produce an intermediate finite state machine and unwinding conditions. This approach provides a uniform framework for reasoning about abstract software system specifications and their implementations. It also allows us to prove security at an abstract level so that changes to programs that do not affect functional behavior will not affect the security proof.