Proposals for
Master thesis
Static Memory Analysis of Java
Smart Cards
Memory Analysis of
Java Smart Cards using
Maude
Programmable smart cards are small personal devices provided with a
microprocessor capable of manipulating confidential data. Smart card
applications are usually written in a high-level Java-like language.
The Java Card Virtual Machine (JCVM) compiles such applications into
bytecode. JVCM is a simplified version of the Java Virtual Machine
(JVM).
Memory is a scarce resource in such devices, hence it is important to
guarantee that an applet will not make the card run out of memory.
Based on an existing implementation of the JVM in Maude (JavaFan, http://fsl.cs.uiuc.edu/javafan/),
the student
will first write a Maude implementation of the JCVM. In a second stage,
the student will implement a bytecode memory analyzer (the
specification of the algorithm may be found in the CLEI paper)
in Maude, in
order to statically determine a bound on the memory used by an
application.
Check the Norwegian description at the
Masteroppgaver ved PMA homepage under the title Minneanalyse av Java smartkort i Maude.
Optimizing
the Memory Consumption Analyser of Project 1
The CLEI paper (the same
base paper of project 1)
introduces the specification of a memory consumption analyser for Java
card bytecode programs which improves -in terms of space complexity- a
previous algorithm (presented in the FM
conference). Since memory is a scarce resource in Java cards, the
auxiliary memory used by the analyser should be as less as possible.
Both algorithms mentioned above still uses more auxiliary memory than
the available in a Java card, but it seems possible to modifiy the
algorithm presented CLEI paper in order to make an on-card analyser
feasible.
The student will study how to improve such algorithm (writing a
constraint-based specification) and implement it.
Formal
(Assisted) Proof of a Memory Analyser for Embedded Java Bytecode
This is a more theoretical project. The proof of soundness and
completeness of the algorithm for memory analysis presented in the CLEI paper (the same base paper of project 1) is based on a maximal semantics -i.e. the
semantics of a bytecode program is given by the set of all possible
(total) execution traces. An alternative way of proving soundness and
completeness would be by using a partial
(or prefix) semantics, where
the semantics of a bytecode program is given by the set of all the
prefix traces. Using such semantics, the correctness (soundness) proof
can be done by showing that the constraints defining the analyser is an
invariant of the prefix semantics of the given program. A previous
memory consumption analysis algorithm has been proved correct in
the proof assistant Coq using this approach (see the FM paper); moreover, a program (running code)
has been extracted from its proof of correctness.
Based on the above-mentioned proof in Coq (the FM paper), the student
will
prove the correctness of the algorithm (given in the CLEI paper)
in Coq with the aim of extract the analyser from its proof.
For a relative short project, the student should be a Coq expert, or at
least have some knowledge about Coq. Otherwise, this project could take
some time...
Compositional
Memory Analysis for Embedded Java Bytecode
This subject is a continuation/improvement of project 1. Approximative
memory analysis of stand-alone applications may be done statically but
it is not the case, in general, for
interacting applications. Guaranteeing a bound on the memory used by an
"open" application, for which its interaction with the environment it
is not known statically, requires some run-time analysis. It is costly
to compose first two application and then make a global analysis at
run-time. It would be desirable to minimize the computation after
composition (which is at run-time and it usually comprises the
computation of a global fixpoint) and to exploit the (static)
computation of local fixpoints as much as possible.
Based on an existing specification of the algorithm, the student will
implement in some
programming language (why not in Maude?) a constraint-based analyzer
for open bytecode applications and (s)he will establish the feasibility
of the approach by comparing the results with the global analysis
(described in project 1).
Verification of Hybrid Systems
A hybrid system is a
system where both continuous and discrete behaviors interact with each
other. A typical example is given by a discrete program that interacts
with a continuous physical environment, like the control program of a
robot. The hybrid nature of such systems (which often involves
differential equations) makes their verification very difficult; in
fact only few problems for restricted sub-classes of hybrid systems are
decidable.
Implementation
of Optimization Techniques for
SPDIs based on Invariance, Controllability and
Viability Kernels
One of the main research areas in verification in general and in
particular in hybrid systems is reachability analysis. While many
interesting properties of hybrid systems may be stated as a
reachability problem, it is not the case in many other cases, in which
a qualitative analysis is
needed. The kind of properties that are usually interesting from the
qualitative point of view are convergence
or stability. For example, do
certain trajectories/curves lie in a bounded part of the plane, are
there lines that separates the plane into regions that are not
``connected'', are some of them closed curves, etc.? Such singular
points, closed curves, separatrix lines, etc., are important objects
giving qualitative information about the hybrid system. The set of all
such objects constitute what is called the phase portrait. It has been shown
that it it possible to compute certain objects of the phase portrait of
polygonal hybrid systems (SPDIs), namely invariance, controllability
and viability kernels. We have recently extended the tool SPeeDI with
the computation of the invariance, controllability and viability
kernels (SPeeDI+). In the FORMATS'06 paper
we have shown that such kernels may be used to reduce the state-space
of reachability analysis of SPDIs. This project comprises the
implementation of the techniques presented in that paper for optimizing
reachability analysis of SPDIs.
SPeeDI is a tool for reachability analysis of SPDIs, completely written
in Haskell. The project consists in extending SPeeDI for computing the
invariance, controllability and viability kernels of SPDIs. See the SPeeDI homepage.
Implementation
of a Compositional Parallel Algorithm for Reachability Analysis of SPDIs
In the paper presented at ICTAC'06 we have
developed a compositional algorithm for solving the reachability
problem for SPDIs in a parallel/distributed manner. This project
intends to implement the algorithm, apply it to case studies and to
compare with the standard DFS algorithm already implemented in SPeeDI.
In order to do so, the student must implement first a BFS algorithm for
SPDI reachability.
Using
SPDIs for Approximating Non-linear Differential Equations
One of the main uses of polygonal hybrid systems SPDIs is to
approximate non-linear differential equations. In this project the
student will use SPDIs to produce good approximations of planar
non-linear differential equations.
Specification and Analysis of
Contract Languages
There are many interesting student projects on the domain of
specification and formal analysis of (conventional and electronic)
contract languages. Please refer to the homepage of the Nordunet3
project "Contract-Oriented
Software Development for Internet Services". Master thesis on
this topics includes specification, model checking, proof systems, and
static analysis, and it ranges from purely theoretical to
implementations.
Go back to
Gerardo Schneider's Homepage