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.
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.
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.