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