This page presents the sources of a prototype mobile code verification framework which can be found as an attachment uploaded to this page. It includes mobile code benchmarks, sample security policies, configuration files and directions for conducting the experiments.  The framework uses a model-checking toolset, SATABS, which implements a  counterexample-guided abstraction refinement for efficient program  verification. A mobile program and a security policy should be provided as input to  the model-checking engine. It is also possible to provide a  configuration file giving details on the initial network configuration.  If the file is not given, the policy is checked against all possible network configurations.

For more information on the verification framework, please refer to [1].

To set up the experimental framework:

1. Download SATABS binaries from http://www.cprover.org/satabs (NB: you need a model checker for SATABS, download one of the  recommended from SATABS web page)

2. Download the mobile code framework mobile_code_framework.tar.gz

3. Untar mobile_code_framework.tar.gz

4. Put a copy of SATABS binaries in the mobile_code_framework and put SATABS in your PATH variable

5. Enter the mobile_code_framework directory and check the README file  for further details.

References