< Back to previous page

Project

Development of information flow policy enforcement techniques.

All software is represented as source code in a programming language. The programming language defines the meaning or semantics of the code, for example, its operational behaviour. Computational source code is often accompanied by additional specifications that define how the source code should be interpreted or provide additional information about the softwares semantics. They make it possible for programmers to express and verify that their software has the intended semantics and to express inter-component semantic assumptions. Good representations and specifications of software components are crucial for efficiently producing software that is reliable, efficient and secure, and for preserving these qualities during the softwares evolution.

Many types of software components and their desired semantic properties can be challenging to represent and specify. In this work, I contribute novel functional techniques for the representation and specification of four types of software components:

  • Ad hoc polymorphic functions: functions whose behaviour depends on the types of their arguments or result. I present instance arguments: a type system extension for representing ad hoc polymorphic functions in the dependently-typed programming language Agda. Compared to existing proposals, instance arguments do not introduce an additional structuring concept and ad hoc polymorphic functions using them are fully first-class. Furthermore, they avoid introducing a separate, powerful form of type-level computation and existing Agda libraries using records do not need modifications to be used with them. My implementation has been part of Agda since version 2.3.0 and I demonstrate a variety of applications of instance arguments
  • Context-free grammars: a standard way to define the syntax of formal languages. I present a technique for representing context-free grammars in an embedded domain-specific language (EDSL). It avoids the restrictions of existing parser combinator libraries using a novel explicit representation of recursion based on advanced type system techniques in the Haskell programming language. As a byproduct, grammars are decoupled from sets of semantic actions. On the flip side, the approach requires the grammar author to provide a type- and value-level encoding of the grammars domain and I can provide only a limited form of constructs like many. I demonstrate the approach with five grammar algorithms, including a pretty-printer, a reachability analysis, a translation of quantified recursive constructs to standard ones, and an implementation of the left-corner grammar
    transform. This work forms the basis of my grammar-combinators parsing library.
  • Meta-programs: programs that generate or manipulate other programs. I present a novel set of meta-programming primitives for use in a dependently-typed functional language. The meta-programs types provide strong and precise guarantees about the meta-programs termination, correctness and completeness. The system supports type-safe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, meta-programs are written in the same style as normal programs and use the languages standard functional computational model. I formalise the new meta-programming primitives, implement them as an extension of  Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.
  • Effect polymorphic software: programs that support arbitrary implementations of effectful APIs and only produce effects through those implementations. Static effectful APIs and global mutable state in object-oriented programming languages make it hard to modularly control effects. Object-capability (OC) languages solve this by enforcing that effects can only be triggered by components that hold a reference to the object representing the capability to do so. I study this encapsulation of effects through a formal translation to a typed functional calculus with higher-ranked polymorphism (I use a subset of Haskell for presentation). Based on an informal view of effect-polymorphism as the fundamental feature of OC languages, I translate an OC calculus to effect-polymorphic Haskell code, i.e. computations that are universally quantified over the monad in which they produce effects. The types of my translations assert the object-capability property and I can show and exploit this using Reynolds parametricity theorem. An important new insight is that current OC languages and formalisations leave one effect implicitly available to all
    code, without a capability: the allocation of new mutable state; adding a capability for it has important theoretical and practical advantages. My work establishes a new link between object-capability languages and the well-studied fields of functional programming and denotational semantics.
Date:22 Jun 2009 →  30 Sep 2014
Keywords:Information flow control, Security, Software, Computer science
Disciplines:Applied mathematics in specific fields, Computer architecture and networks, Distributed computing, Information sciences, Information systems, Programming languages, Scientific computing, Theoretical computer science, Visual computing, Other information and computing sciences
Project type:PhD project