论文标题
使用类型修饰符的信息流控制的信息流控制对象的语言
Information Flow Control-by-Construction for an Object-Oriented Language Using Type Modifiers
论文作者
论文摘要
在关键安全软件应用程序中，必须防止机密信息泄漏到未经授权的水槽。静态分析技术是广泛的，可以通过在施工后检查程序来实施安全信息流。这些系统的缺点是无法正确检查施工过程中的不完整程序。大多数系统并未将用户引导到安全程序。我们介绍了IFBCOO，这是一种通过使用改进规则逐步指导用户进行安全实现的方法。在每个完善步骤中，保密性或完整性（或两者都可以保证）与程序的功能正确性一起，以便通过施工降低了不安全的计划。在这项工作中，我们将IFBCOO形式化并证明了改进规则的健全性。我们在工具中实施IFBCOO，并通过成功实施案例研究来进行可行性研究。
In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies.
