Program analysis
Static program analysis aims at
determining properties of the behaviour of a program without actually
executing it. Static analysis is founded on the theory of abstract
interpretation for proving the
correctness of analyses with respect to the semantics of a programming
language.
My work has among other things been concerned with
- type-based static analysis
- analyses for the particular language
paradigms (in particular functional and object-oriented)
- control-flow analysis of programs,
used e.g. in the activity on
software security.
Recently, I have been investigating how static analysers can be
designed using contructive logic in order to extract certified static
analysers from their mechanically checked specifications.
Static analysis can be used to built a Proof-Carrying Code
infrastructure where advanced static analysers can be used to construct
program invariants that can be checked by simpler, and mechanically
checked verifiers. Here is a paper describing such an architecture
|
Software security
The particular branch of information
security called "language-based security" is concerned with the
study of programming language features for ensuring the security
of software. Programming languages such as Java offer a variety
of language constructs for securing an application. Verifying that
these constructs have been
used properly to ensure a given security property is a challenge for
program
analysis,
I have been working of various versions of embbed Java, including Java
Card and Java for mobile telephones. Here
is an article (to appear in J. Computer Security) with a proposal for a
more flexible
access control mechanism for Java enabled moble telephones that is more
amenable to static verification.
Java security can be further enhanced by extending the static byte code
verification to other properties. At ByteCode 2009 I gave an invited talk about how this can be made
feasible using software certificates generated by static
analysis.
|
