Java Hybrid Analysis Version 0.5

PDF

Authors
  1. Painchaud, F.
Corporate Authors
Defence R&D Canada - Valcartier, Valcartier QUE (CAN)
Abstract
This document proposes a new program analysis technique, called hybrid analysis, that combines both static and dynamic analysis principles. It is currently being developed to ensure the security of Java programs in the context of critical military information systems. This new program verification technique is theoretically sound and precise, which constitutes a major contribution to the formal program verification domain. At this stage, Java hybrid analysis is based on finite state automata theory and firstorder predicate logic, only succinctly covered in this document. The reader is thus assumed to be relatively familiar with these domains. However, the precise model and logic used by Java hybrid analysis are extensively described. Furthermore, five different hybrid analysis approaches have been devised. They have been given the following names: interactive hybrid analysis, parameterized hybrid analysis, test-based hybrid analysis, worst-case hybrid analysis, and statically-supported dynamic analysis. A small case study is presented in order to illustrate the concepts behind the first approach. Finally, a discussion depicts the future of this approach. The Java hybrid analysis detailed in this document is labeled version 0.5 to depict the fact that it is still unstable and evolving.

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

Keywords
C2IS Certification;Java;Java Security;Static Analysis;Dynamic Analysis;Hybrid Analysis
Report Number
DRDC-VALCARTIER-TM-2004-060 — Technical Memorandum
Date of publication
01 Feb 2007
Number of Pages
46
DSTKIM No
CA029151
CANDIS No
527372
Format(s):
CD ROM

Permanent link

Document 1 of 1

Date modified: