A logic for information flow in object-oriented programs
A logic for information flow in object-oriented programs
复制标题
DOI：
10.1145/1111037.1111046
复制
发表时间：
2006-01
期刊：
影响因子：
--
通讯作者：
Torben Amtoft;Sruthi Bandhakavi;A. Banerjee
中科院分区：
文献类型：
--
作者：
Torben Amtoft;Sruthi Bandhakavi;A. Banerjee
本文通过类似霍尔的逻辑，详细说明了面向对象程序的过程间和流敏感（但终止不敏感）信息流分析。指针别名在此类程序中普遍存在，并且可能会泄露机密信息。因此，该逻辑采用独立断言来描述形式化机密性的非干扰属性，并采用区域断言来描述可能的混叠。还允许 JML 风格的程序员断言，从而允许更细粒度的信息流策略规范。逻辑支持分离逻辑风格的有关状态的本地推理。采用小规格；他们只提到与命令相关的变量和地址。使用框架规则组合规格。描述了一种计算后置条件的算法：在某些假设下，存在该算法计算的最强后置条件。
This paper specifies, via a Hoare-like logic, an interprocedural and flow sensitive (but termination insensitive) information flow analysis for object-oriented programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs independence assertions to describe the noninterference property that formalizes confidentiality, and employs region assertions to describe possible aliasing. Programmer assertions, in the style of JML, are also allowed, thereby permitting a more fine-grained specification of information flow policy.The logic supports local reasoning about state in the style of separation logic. Small specifications are used; they mention only the variables and addresses relevant to a command. Specifications are combined using a frame rule. An algorithm for the computation of postconditions is described: under certain assumptions, there exists a strongest postcondition which the algorithm computes.