一句话：提出面向对象语言 SIFO，用不可变性与唯一性类型修饰符提升信息流控制精度，证明非干扰性并实现为可插拔类型系统。
安全关键的软件常包含机密信息，需防止其泄露给未授权系统。基于语言的信息流控制（如类型系统）可强制执行机密性策略，但面向对象语言中的精度问题突出：需在可靠保持非干扰性的同时，避免拒绝过多安全程序。本文提出面向对象语言 SIFO，通过类型修饰符利用对象的不可变性与唯一性来检测信息泄露，从而提高类型系统精度。作者以示例非形式化介绍 SIFO，形式化其类型系统并证明非干扰性，将其实现为 L42 中的可插拔类型系统，并通过可行性研究与基准测试进行评估。
Security-critical software applications contain confidential information which has to be protected from leaking to unauthorized systems. With language-based techniques, the confidentiality of applications can be enforced. Such techniques are for example type systems that enforce an information flow policy through typing rules. The precision of such type systems, especially in object-oriented languages, is an area of active research: an appropriate system should not reject too many secure programs while soundly preserving noninterference. In this work, we introduce the language SIFO which supports information flow control for an object-oriented language with type modifiers. Type modifiers increase the precision of the type system by utilizing immutability and uniqueness properties of objects for the detection of information leaks. We present SIFO informally by using examples to demonstrate the applicability of the language, formalize the type system, prove noninterference, implement SIFO as a pluggable type system in the programming language L42, and evaluate it with a feasibility study and a benchmark.
@article{paperbot2140,
title = {Immutability and Encapsulation for Sound OO Information Flow Control},
author = {Tobias Runge and Marco Servetto and Alex Potanin and Ina Schaefer},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {1},
year = {2023},
doi = {10.1145/3573270}
}