Verifier of Mobile Code Security

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 an 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 informations on the verification framework, please refer to [1].

To set up the experimenal framework:
1. Download SATABS binaries from http://www.cprover.org/satabs/
(NB: you need a model checker for SATABS, download one of the  reccomended 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