| Security and privacy are of increasing concern as information is made available on the Web and computers are exposed to attacks from hostile machines that may be located anywhere on the planet. There is a need for reasonable assurances for software applications that execute in this context. Information flow control refers to providing some assurance that sensitive information is not being leaked to hostile agents.;This thesis proposes several new tools for reasoning about information flow control, motivated by the challenges and threats of distributed systems. The first tool is an adaptation of transactional semantics to facilitate coordination between both trusted and untrusted processes in concurrent and distributed applications. Secure nested transactions are introduced to provide a new programming model for such applications. This model is proposed as an extension of the methodology associated with information flow control in sequential programs. The model includes a new notion of retroactive aborts as a fundamental part of its semantics.;The second tool is an extension of the Java programming language, that allows security policies and information flow policies to be expressed in the type systems and enforced through a combination of static (compile-time) and dynamic (run-time) mechanisms. This extension introduces the Jeddak language, which constitutes an experiment in providing language-based mechanisms for secure distributed applications. The thesis work involves examining practical applications from the Java software base, determining what mechanisms are needed to support compiler-based reasoning about security properties, and proving the correctness of those mechanisms when added to the language semantics. |
