wiki:projects/jpf-mango

Mango

Vulnerability Testing demo

Mango Talk Slides, April 9, 2013 tool feature demo, including the new class resolver for code approximation

Vulnerability Example discussion of training and test results

Test Generation example presented at the JPF-Workshop 2012

Slides and transcript

Mango is a Java™ assurance tool, deployed as an Eclipse workbench plugin. Mango is developed as the jpf-mango extension of JPF.

Capability

Mango builds a functional model of Java code, exposed as navigable browser pages. When used as a sanity checker, Mango will halt at every case-split, allowing the programmer to compare source code with generated model. The functional view of code is often quite different from the code itself, and potentially reveals hidden flaws.

Mango may be of value as an educational tool. Those learning Java as a first programming language have the opportunity to compare procedural and functional views of code. This comparison facilitates the exposition of formal modeling concepts. For this purpose, the Mango installation contains a comprehensive set of first year Java code examples, together with the corresponding Mango formal models.

Mango may potentially be used to generate and apply filters for known Java security issues. Oracle has published a set of secure programming guidelines. The idea is to apply Mango to code snippets exposing potential security problems. By analyzing the corresponding formal model, it is be possible to develop rules to recognize security issues. Mango has a highly sophisticated rule-based generalized pattern matching capability to enable such rule development. This is currently an active area of Mango development, see Test Generation

The Mango formal model may be translated into ACL2, an automated theorem proving language. In the past, formal proofs of Mango generated conjectures have been accomplished. Mango was originally created for this purpose, and this direction represents the future. But in all honesty a lot of work remains before tangible results may emerge. Anyone interested in pursuing this line of thought should contact the principal Mango developer, frankrimlinger+mango at gmail.com.

Mango was presented as a "formal advisor" at the 2011 JFP Workshop. The paper A Formal Advisor for Eclipse Java Development and corresponding slides give a technical overview of Mango.

Installation

To use Mango, it is only necessary to install the plugin. Certainly this will suffice for learning the basic operation of Mango. Actual application of Mango to a real project will probably require the feedback and flexibility of the Mango development platform. The recommendation at this point is to first install the plugin to learn the Mango basics, and then switch to the development platform for more serious work.

System requirements

The plugin and development platform for Mango have been tested on the most current versions, as of April 27, 2012, of MacOSX, RedHat, and Ubuntu, using the latest release of the Eclipse workbench, Indigo.

**NOTICE 7/9/2012** STABLE. plugin release 1.0.31. Runs on Eclipse Juno, not backward compatible with earlier releases, i.e. Indigo.

Mango should run anywhere the Eclipse workbench can be installed, assuming the underlying file system has Unix-like capabilities. Unfortunately, on Windows there is a hard limit of 260 characters on the length of a path name, which currently is a show-stopper for Mango. Mango relies on internals of jpf-core and the Eclipse platform itself, and these change over time, requiring changes in Mango. Every reasonable attempt will be made to keep Mango compatible with previous versions of its own database structure, but no guarantees. The plan is for active Mango development to support the most recent versions of jpf-core and the Eclipse workbench running on MacOSX, RedHat, and Ubuntu. However, the project is officially provided "as is", see the license for details.

Installing the Mango plugin

In order to use Mango, the Mango plugin must be installed in the Eclipse workbench.

Click here for Mango plugin installation instructions.

Installing the Mango development platform

Installing the development platform allows the user to create bug reports for problems. More advanced users may also extend Mango functionality and trace Mango execution.

Click here for Mango development platform installation instructions.

Getting started

Click here for a step-by-step exposition of the "Hello World" example for Mango.

Examples

CarRecall

The Mango plugin installation contains various example projects. The largest of these projects is FirstYearCode, which contains example code from a high school Java course. Within FirstYearCode, the CarRecall example illustrates how Mango reports case-splits and loops. There are about sixty such examples in the FirstYearCode package. Mango builds the specification for fifty of these. The other ten contains errors, see bug #3 and the "First year status" attachment to this page. The procedure for generating and rendering the CarRecall specification is basically the same as the Hello World example, but more user interaction is available to incrementally reveal the case-split structure of the code.

CarRecall exposition.

ItsAWrap

The testCode/rbk directory contains projects written with the intent of proof artifacts for ACL2. For one example, ItsAWrap, proof artifacts were in fact generated and actual proofs in the ACL2 logic were accomplished. However, the code within Mango for this pipeline is currently broken, see bug #6. The exposition of ItsAWrap shows how the user can introduce hypotheses into Mango to guarantee loop termination. Ideally, such hypotheses should be generated automatically, see bug #7.

ItsAWrap exposition.

Sample Sync Adapter

Several classes of the Android Sample Sync Adapter code have also been specified using Mango. In particular, the Test Generation example uses some representative code to demonstrate how the tool can be trained to detect vulnerabilites. This example lays the groundwork for automated testing of security properties, as discussed above.

User Manual

Control Mango with the Mango Explorer buttons.

Control the scope of a specification build.

Moderate specification behavior using Mango preferences.

Report a bug.

Delete the gutter icons.

Display a spec whose gutter icon is deleted.

Synchronize MangoHome with the file system.

Recover from a spec failure.

Serially specify multiple targets.

Replay an existing spec.

Customize specification generation with shadow rules.

Resolve a formal link error.

Swap in a different MangoHome + MangoSystem.

Swap in individual modules from a different MangoHome (storeConfig regeneration).

Write a rule.

Develop new rule actions.

History of Mango

To gain a sense of how Mango has evolved, a look at the Archived Examples is instructive. The following was written in 2008 at the beginning of the Mango project.

Purpose: To provide a case by case specification of Java™ source code, analogous to Javadoc but more rigorous.  To provide "proof artifacts" to a theorem prover, enabling the mathematical proof of code properties.

Ultimate Goal: To integrate the generation of code, specification, and correctness proofs so that a programmer may produce a more reliable product with the same level of effort.

Theory of Operation:  The code is first converted to a large graph of vertices (instructions) and directed edges (branch conditions), often referred to as the flow control diagram.  This conversion occurs at the byte code level, which is convenient because the byte codes are described very succinctly in terms of the state of the Java Virtual Machine (JVM).  This conversion is essentially accomplished by the JPF core engine.  The Mango formal peer code then generates for each byte code a description in terms of the Mango formal model.  A graph subdivision algorithm is applied to the control flow, generating a hierarchical sequence of graphs required to describe the loops within the code as recursive functions.  JPF is then used to walk these graphs for the purpose of generating the specification and proof artifacts.  The backtracking ability of JPF is utilized to generate cases, and the ability to trace back along trails is leveraged in order to compute loop invariants.  Ideally, the process would be fully automated, but in practice when Mango requires guidance from the user, JPF will block and a gui thread will interact with the user to obtain the information required to proceed.  The specification and proof artifacts are stored in persistent form exposed to the user in a rule base format, enabling reuse and incremental, distributed operation.

Limitations:  Mango only specifies "good" cases, exposing input constraints required to satisfy such cases.  Some user guidance is required to determine what constitutes a good case.  It may happen that even the number of good cases grows exponentially.  The user must then provide case generalization logic to abstract away explosive case growth.  Such abstractions must also be accompanied by type and translation logic, which the user must provide.  Although Mango does generate loop termination conjectures, such conjectures are generally in terms of loop output.  Typically the user must provide guidance to form hypotheses for loop termination in terms of loop inputs.  Correctness of such hypotheses may be confirmed by an automated theorem prover, which typically requires expert guidance.

Status:  Mango is based on technology released by the Nasa/Ames Software Release Authority in September, 2008.  Much of the original code base was written in C++.  By Spring, 2009, the code base was migrated to 100% pure Java, and integrated with Eclipse RCP, the rich client platform.  The original code base did not use JPF.  Full integration with JPF commenced in the Summer of 2009 and should be complete by January 2010.  The tool should achieve an initial operational capability by Spring 2010.  Ultimately, the tool will be deployed as an Eclipse workbench plugin.

Research: Previous versions of the tool did generate artifacts for the ACL2 theorem prover and substantial proofs were accomplished.  Efforts are just getting started to lightly embed the current Mango model in ACL2.  However, the proof artifacts are essentially just expressions in the Mango model of definitions, hypotheses and conjectures, and as such are theorem prover neutral.  There is no automatic facility for generation of hypotheses on loop inputs required to prove termination.  Needless to say, this is a fundamental tool weakness and contributions in this area would be most welcome.  (Caveat emptor: there is no general purpose algorithm for determining loop termination, but constructive solutions exist for typical circumstances.)

Last modified 3 years ago Last modified on 02/25/2014 08:27:26 PM

Attachments (7)