Combining Static and Dynamic Analysis for Advanced Certification of Java™ C2IS


  1. Painchaud, F.
Corporate Authors
Defence R&D Canada - Valcartier, Valcartier QUE (CAN)
Since information-processing systems are becoming omnipresent in our daily lives and in safety-critical infrastructures, there is a strong move to validate and verify them, in order to make them more fault-tolerant and secure. To meet this challenging objective, it is believed that formal methods must be included within the hardware and software engineering processes, which presently suffer from having insufficient (although growing) tool-support with a sound mathematical foundation. Static and dynamic analysis, certifying compilation, and model checking are good examples of such formal methods for hardware and software validation and verification. This document first presents a summary of two successfully completed projects on malicious code detection and Java certifying compilation, which used formal methods to certify software packages for security purposes. This is followed by an introduction to model checking and Abstract State Machines as a basis for this project. This new project aims at defining and implementing a novel hybrid model-checking approach for Java. This approach is hybrid in the sense that it combines static and dynamic analysis principles in order to provide more precise model checking. Ultimately, this project is therefore about using Abstract State Machines (more precisely, the Abstract State Machine Language) as a modeling formalism for Java programs, developing a model checker for this formalism, and parameterizing this model checker in the hope of be

Il y a un résumé en français ici.

Software Certification;Java;Java Security;Static Analysis;Dynamic Analysis;Abstract State Machines;Model Checking;Data processing security;Malicious code;Program verification;Software security;Java security architecture
Report Number
DRDC-VALCARTIER-TM-2004-001 — Technical Memorandum
Date of publication
01 Mar 2004
Number of Pages

Permanent link

Document 1 of 1

Date modified: