Type Based Techniques for Covert Channel Elimination and Register Allocation

• As the title suggests, this thesis consists of two parts that address two rather different topics. The first part investigates secure information flow in sequential programs, with the aim of completely eliminating covert timing channels. The second part presents a technique to describe register allocation for a functional language. Common to both parts is that the techniques described make heavy use of types and type-based program analysis. Covert Channel Elimination refers to the work presented in papers I and II, which both deal with the removal of covert timing channels through program transformation. The setting and motivation is that of confidentiality in mobile code. Given a program from an untrusted source, the sensitive data it manipulates must not be leaked to unauthorised agents, observing the programs execution through its network accesses. In paper I, a type system is developed for a small while-language, where well-typed programs obey a time-sensitive noninterference property and are secure in the sense that they do not leak confidential information directly, indirectly or through their temporal behaviour. A type-based transformation that eliminates covert timing channels is also presented. The soundness and correctness of the approach is proven formally. Paper II moves the context of timing leak elimination down to a more practical level. Experiences from the implementation of a timing leak eliminating transformation for a subset of Java byte code are presented. The problems involved in adapting the transformation formalised for a while-language in Paper I, to a machine language are discussed and the solutions chosen in our implementation are presented. Paper III discusses the construction of secure programs and the consequences of noninterference on algorithmic complexity. The paper argues that for algorithms that manipulate pointers to secret data, support from the runtime system (and/or compiler) is necessary to mask the execution time effects of cache behaviour. The paper also argues that even with such support, noninterfering algorithms for searching a collection of secret objects cannot be made faster than OMEGA(log n). In Part II of the thesis, Paper IV presents a typed functional language with explicit register usage. The language is intended as an intermediate representation for use in a compiler, and can be seen as a lambda-calculus with strong flavours of assembly language. A type and effect system is used to monitor the use of registers. The soundness property of the system is that well typed terms will not overwrite registers containing live data.

Subject headings

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Keyword

type and effect systems

program analysis

functional languages

confidentiality

register allocation

privacy

computer security

covert timing channels

program transformation

information flow

type systems

Publication and Content Type

dok (subject category)

vet (subject category)