JFlow: Practical Mostly-Static Information Flow Control

JFlow: Practical Mostly-Static Information Flow Control

1999 | Andrew C. Myers
JFlow is a practical, mostly-static information flow control language that extends Java to allow static checking of flow annotations. It introduces a decentralized label model, label polymorphism, run-time label checking, and automatic label inference, making information flow checking more flexible and convenient than previous models. JFlow supports complex language features such as objects, subclassing, dynamic type tests, access control, and exceptions, which have not been successfully integrated with static information flow control. The language provides a simple but powerful model of access control, allowing code privileges to be checked statically and dynamically. JFlow also supports safe, statically-checked declassification, allowing principals to relax their privacy policies without weakening others. The JFlow compiler is a source-to-source translator, producing standard Java code that can be compiled by any Java compiler. Most checking is static, resulting in minimal code, data, or runtime overhead. The paper describes the JFlow language, its formal rules, and the translation process. It also discusses the use of JFlow in secure servers and applets. JFlow's decentralized label model allows multiple principals to protect their privacy even in the presence of mutual distrust. The paper also discusses the limitations of JFlow, including the inability to eliminate all possible information leaks and the challenges of controlling covert channels such as timing channels and hash code channels. JFlow provides a way to manage run-time labels, as demonstrated in the Protected class example. The paper concludes that JFlow is a practical language for information flow control, with a focus on usability and flexibility.JFlow is a practical, mostly-static information flow control language that extends Java to allow static checking of flow annotations. It introduces a decentralized label model, label polymorphism, run-time label checking, and automatic label inference, making information flow checking more flexible and convenient than previous models. JFlow supports complex language features such as objects, subclassing, dynamic type tests, access control, and exceptions, which have not been successfully integrated with static information flow control. The language provides a simple but powerful model of access control, allowing code privileges to be checked statically and dynamically. JFlow also supports safe, statically-checked declassification, allowing principals to relax their privacy policies without weakening others. The JFlow compiler is a source-to-source translator, producing standard Java code that can be compiled by any Java compiler. Most checking is static, resulting in minimal code, data, or runtime overhead. The paper describes the JFlow language, its formal rules, and the translation process. It also discusses the use of JFlow in secure servers and applets. JFlow's decentralized label model allows multiple principals to protect their privacy even in the presence of mutual distrust. The paper also discusses the limitations of JFlow, including the inability to eliminate all possible information leaks and the challenges of controlling covert channels such as timing channels and hash code channels. JFlow provides a way to manage run-time labels, as demonstrated in the Protected class example. The paper concludes that JFlow is a practical language for information flow control, with a focus on usability and flexibility.
Reach us at info@study.space
Understanding JFlow%3A practical mostly-static information flow control