Research Focus
Programming
languages lie at the heart of techniques for developing secure and reliable
software. My research interest is in the general area of programming languages,
including both theory and practice. I focus on applying formal techniques to
the real-world problems of software security. I am also interested in
compilers, database, logics, process calculi, automatic theorem proving,
distributed and concurrent systems.
My long-term
vision is to develop advanced programming language features and tools to enable
programmers to build more reliable, high performance and low cost software. Such
software will have provable finer-grained security properties, and client
applications and devices will be able to check the desired security properties
via a dynamic but lightweight verification.
Previous Research
One of the
major problems in reasoning with object-oriented code, such as Java, has been
the difficulty in coping with object aliasing in a modular fashion. Informally
the problem is that pointers (or references) are not constrained by lexical
scope, and therefore any program logic will have difficulty in dealing with
them. As a result, pointer aliases are ubiquitous in programs and can
potentially leak confidential information. They have also made reasoning about
program correctness very difficult and may interfere with reuse objectives of
software components. My work on alias/effect reasoning and access control,
following the track of previous research on object encapsulation and ownership
types, tries to localize pointers and side effects to allow program logics to
offer localized reasoning for program invariants.
Object
encapsulation mechanisms have established a tradition for solving the problem
of representation exposure based on a principle of reference containment. I
proposed a new principle, effect encapsulation, which confines side effects,
rather than object references, according to an ownership structure. Compared to
object encapsulation, effect encapsulation liberates us from the restriction on
object referenceability and offers more flexibility.
In follow-up
work, I designed a general framework for reasoning about object invariants
based on a behavioural abstraction that specifies two sets---the validity invariant and the validity effect. The overlap of these
two sets captures precisely those objects that need to be re-validated at the
end of the behaviour. I also designed a type system based on this framework,
which uses ownership types to confine dependencies for object invariants, and
restricts permissible updates to track where object invariants hold even in the
presence of re-entrant calls, but otherwise object referenceability and read
access are not restricted.
Classic
ownership type systems impose fixed ownership and an inflexible access policy.
In other work, I designed a small programming language which is able to provide
a static context that specifies a per-object access control policy for
references. Compared with Java's class-level field access control, my language
offers instance-level object access control. It can be used to restrict access
to sensitive data, secure information flow, as well as provide data abstraction
for easier software maintenance.
The desire for
compile-time knowledge about the structure of heap contexts is currently
increasing in many areas. However, approaches using whole program analysis are
too weak in terms of both efficiency and accuracy. I designed a new type system
that enforces programmer-defined constraints on reachability via references or
pointers, and restricts reference cycles to be within definable parts of the
heap. Such constraints can be useful for program understanding and reasoning
about effects and invariants, for information flow security, and for run-time
optimizations and memory management.
Research
Directions
The idea of
object ownership has been used in specification languages such as JML and
Spec#. The Boogie methodology, as manifested in Microsoft Research’s Spec#, is based
on a program logic accompanied by a model for protecting the validity of object
state, which dynamically tracks the ownership of objects. Integration of a
Spec#-like program verification system with a type system which statically
captures validity contracts would be an interesting direction to move on.
Information
flow security concerns with protecting confidentiality of data. I am interested
in designing a generalized framework which unifies fine-grained information
flow policies with flexible downgrading policies, data and code access control
policies. Those policies can be specified in a practical object-oriented
language and can be statically enforced by mechanisms such as type systems and
program analysis.
Modern
software relies increasingly on component programming and software libraries.
However, existing interprocedural analysis techniques require whole program
knowledge to be accurate and efficient. Figuring out the right way to handle
incompleteness of programs is important for developing new analysis techniques
for modular software. I am interested in developing
methods using a combination of static analysis and type system techniques to
perform more precise alias analysis and information flow analysis in incomplete
object-oriented programs, especially Java bytecode.
I am also
interested in problems outside these realms. Especially, I am interested in
exploring the use of ownership-like type systems to localise processes and
control access in concurrent programs and Pi-calculus based systems.