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