I have moved to the University of Calgary. Your browser will be redirected to my new page in 5 seconds, or you can following this link directly.
This work represents a critical rethinking of the Java bytecode verification architecture from the perspective of a software engineer. In existing commercial implementations of the Java Virtual Machine, there is a tight coupling between the dynamic linking process and the bytecode verifier. This leads to delocalized and interleaving program plans, making the verifier difficult to maintain and comprehend. A modular mobile code verification architecture, called Proof Linking, is proposed. By establishing explicit verification interfaces in the form of proof obligations and commitments, and by careful scheduling of linking events, Proof Linking supports the construction of bytecode verifier as a separate engineering component, fully decoupled from Java's dynamic linking process. This turns out to have two additional benefits: (1) Modularization enables distributed verification protocols, in which part of the verification burden can be safely offloaded to remote sites; (2) Alternative static analyses can now be integrated into Java's dynamic linking process with ease, thereby making it convenient to extend the protection mechanism of Java. These benefits make Proof Linking a competitive verification architecture for mobile code systems. A prototype of the Proof Linking Architecture has been implemented in an open source Java Virtual Machine, the Aegis VM (http://aegisvm.sourceforge.net).
On the theoretical side, the soundness of Proof Linking was captured in three correctness conditions: Safety, Monotonicity and Completion. Java instantiations of Proof Linking with increasing complexity have been shown to satisfy all the three correctness conditions. The correctness proof had been formally verified by the PVS proof checker.
Philip W. L. Fong. Link-Time Enforcement of Confined Types for JVM Bytecode. To appear in Proceedings of the Third Annual Conference on Privacy, Security and Trust (PST'05), St. Andrews, New Brunswick, Canada, October 12-14, 2005. A preliminary version of the paper appears as Technical Report CS-2004-12, Department of Computer Science, University of Regina, Regina, Saskatchewan, Canada. ISBN 0-7731-0505-0. December 2004. [postscript] [pdf]
Philip W. L. Fong. Pluggable verification modules: An extensible protection mechanism for the JVM. In Proceedings of the 19th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'04), pages 404-418, Vancouver, B.C., Canada, October 24-28, 2004. [postscript] [pdf]
Philip W. L. Fong. Proof Linking: A Modular Verification Architecture for Mobile Code Systems. PhD Dissertation, School of Computing Science, Simon Fraser University, Burnaby, BC, Canada V5A 1S6, January 2004. [postscript] [pdf]
Philip W. L. Fong and Robert D. Cameron. Proof linking: Distributed verification of Java classfiles in the presence of multiple classloaders. In Proceedings of the USENIX Java Virtual Machine Research and Technology Symposium (JVM'01), pages 53-66, Monterey, California, USA, April 23-24, 2001. [postscript] [pdf]
Philip W. L. Fong and Robert D. Cameron. Proof linking: Modular verification of mobile programs in the presence of lazy, dynamic linking. ACM Transactions on Software Engineering and Methodology, 9(4):379-409, October 2000. [postscript] [pdf]
Philip W. L. Fong and Robert D. Cameron. Proof linking: An architecture for modular verification of dynamically-Linked mobile code. In Proceedings of the Sixth ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE'98), pages 222-230, Orlando, Florida, USA, November 3-5, 1998. [postscript] [pdf]
Software execution environments like operating systems, mobile code platforms and scriptable applications must protect themselves against potential damages caused by malicious code. Monitoring the execution history of the latter provides an effective means for controlling the access pattern of system services. Several authors have recently proposed increasingly general automata models for characterizing various classes of security policies enforceable by execution monitoring. An open question raised by Bauer, Ligatti and Walker is whether one can further classify the space of security policies by constraining the capacities of the execution monitor. This paper presents a novel information-based approach to address the research problem. Specifically, security policies are characterized by the information consumed by an enforcing execution monitor.
By restricting the execution monitor to track only a shallow history of previously granted access events, a precise characterization of a class of security policies enforceable by restricted access to information is identified. Although provably less expressive than the general class of policies enforceable by execution monitoring, this class does contain naturally occurring policies including Chinese Wall policy, low-water-mark policy, one-out-of-k authorization, assured pipelines, etc. Encouraged by this success, the technique is generalized to produce a lattice of policy classes. Within the lattice, policy classes are ordered by the information required for enforcing member policies. Such a fine-grained policy classification lays the semantic foundation for future studies on special-purpose policy languages.
Philip W. L. Fong. Access control by tracking shallow execution history. In Proceedings of the 2004 IEEE Symposium on Security and Privacy (S&P'04), pages 43-55, Berkeley, California, USA, May 9-12, 2004. [postscript] [pdf]
Secure cooperation is the problem of protecting mutually suspicious code units within the same execution environment from their potentially malicious peers. A statically enforceable capability type system, called Distributed Data Flow Control, is proposed for the JVM bytecode language to provide fine-grained access control of shared resources among peer code units. The design of the type system is inspired by recent advances in alias control type systems for object-oriented programming languages. Specifically, very capability type specifies a transition system via a syntax resembling the sequential fragment of CSP, whereby transitions are triggered by alias creation events. A capability type thus assigns to an object reference a data flow trajectory, prescribing the set of aliasing event sequences that is allowed to occur to the reference. An orthogonal and complementary annotation system, called Discretionary Object Confinement, is also proposed to counter a class of capability spoofing attacks. The combined type system successfully addresses a number of classical protection problems recast in a programming language context. This work therefore demonstrates the need and the feasibility of a language-based approach to enforce application-level security among peer code units.
Philip W. L. Fong and Cheng Zhang. Capabilities as Alias Control: Secure Cooperation in Dynamically Extensible Systems (Extended Abstract). Technical Report CS-2004-3, Department of Computer Science, University of Regina, Regina, Saskatchewan, Canada. ISBN 0-7731-0479-8. Working draft: [postscript] [pdf].
Philip W. L. Fong and Boting Yang. Discretionary Object Confinement: A Minimalist Approach to Capabilities for the JVM. Technical Report CS-2004-13, Department of Computer Science, University of Regina, Regina, Saskatchewan, Canada. ISBN 0-7731-0506-9. December 2004. [postscript] [pdf]
$Id: index.html,v 1.29 2009/05/28 03:34:44 pwlfong Exp $