Philip Fong's Research

pwlfong@cs.uregina.ca

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.

Table of Contents

Proof Linking

A Modular Verification Architecture for Mobile Code Systems

Abstract

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.

Publications

An Information-based Characterization of Security Policies

Abstract

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.

Publications

Capability Type Systems for Secure Cooperation in Dynamically Extensible Software Systems

Abstract

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.

Publications

$Id: index.html,v 1.29 2009/05/28 03:34:44 pwlfong Exp $

Valid XHTML 1.0!