STAN - STatic Alias aNalyser ---------------------------- STAN is a Java abstract analyser that allows static alias analysis and checking of information flow. Moreover, STAN targets small systems, like embedded systems. The STAN tool statically checks already compiled source code and annotates the .class files with verifiable signatures at loading time. These are the main features of STAN: - dedicated to embedded systems and adapted to their constraints - supports mobile code - easy to use STAN was and is being developed by Yann Hodique and Dorina Ghindici during their phD thesis at LIFL laboratory, University of Lille 1. The instalation directory contains the following sub-directories: - src : the complete source code - src-bcel : sources for bcel library - doc : - lib : needed jar files - bin : scripts to run the application - tests : examples Requirements ------------ STAN builds on Unix and on Windows (using CygWin http://www.cygwin.com/). STAN is compiled using the Ant build tool (http://jakarta.apache.org/ant). It requires Jdk 1.5.0 to work. You must ensure that java, javac are in you path. STAN distribution contains the files regexp.jar and getopt.jar, files required to build it. STAN uses the BCEL library (http://jakarta.apache.org/bcel/) to manipulate .class files and interpret java bytecode. We have modified the original distribution of BCEL in order to generate annotated .class files. How to build ------------ STAN is build using Ant building tool. Follow the steps: 1. Ensure you have installed ant 2. Ensure you have at least jdk 1.5.0 and that you have java and javac in your path 3. Go to instalation directory (directory containing the build.xml file) $cd STAN 4. Run ant to compile the project $ant This command will - compile the src-bcel directory and the resulting .class files will be stored in build-bcel. - compile the src directory and the resulting .class files will be stored in build. You are now ready to run STAN. We suggest to try to run the purse example in tests/purseApp directory. See "How to run an example" section later in this document How to run ---------- The if_analyse script in bin directory permits to perform the analysis. To execute the script: $cd bin $if_analyse Where possible options include: -h/--help : print this help -v/--verbose : verbose mode, print messages -p/--path : use as path for files below -d/--dictionary : use as dictionary -i/--initial-dictionary : use as initial dictionary (for hand annotations) -P/--policy : use as file policy (e.g. containing secret attributes) -H/--hand-annotations : use as file containing hand written annotations -a/--annotate : annotate the .class files -r/--annotate-rep : use as a basis for annotated class dumps -s/--statistics : produce statistics -o/--statistics-file : use as statistics output -t/--html : produce html dumps -b/--html-rep : use as a basis for html dumps -c/--configuration : use the configuration from config.xml -w/--worst-signature : use the worst signature as global signature for abstract methods -x/--directory : analyze all .class files in and its subdirectories -f/--file : analyze all .class files whose names are listed in file The script will run the analysis on the set of classes passed as arguments and/or the .class files in the directory specified by the -x option. config.xml file in bin directory contains predefined configurations. To use one of these configurations, the 'name' attribut of tag must be specified with the option -c/--configuration. Examples of how to use: ./if_analyze -x ../tests/jits/build/fr/ -c jits ./if_analyze -x ../tests/purseApp/ -c purse ./if_analyze -x ../tests/if_tests/simple_tests/ -c test1_analyse Tools ----- The result of the analysis will be a dictionary containing signatures for methods of analysed classes. We offer some tools (under bin directory) to handle the dictionary. bin/if_displayDico : displays the content of a dictionary -h/--help -d/--dictionary : the dictionary -m/--method : display the signatures for method in the dictionary if no method if specified, displays all the dictionary bin/if_inspectDico : analyses the impact of classes passed as arguments onto specified dictionary. Verifies if methods signatures leak infomations. possible options include: -h/--help : print this help -d/--dictionary : use as dictionary -p/--policy : use file as policy -x/--directory : analyze all .class files in and its subdirectories How to start ------------ To better understand this tool , we suggest to start reading the Description.html document in the same directory as this README file. There you can find a brief description of the way algorithm works. To run an example, please refer to section 'How to run an example'. How to run an example --------------------- In this section we will explain how to run an example: the purseApp under tests directory. The electronic purse (http://www.ing.unipi.it/~d8669/SFT/example_sft.html) is a simple java aplication that performs debit/credit operations and some administration functions. In order to test the purse application, we provide a dictionary containing an already analyzed java api (the JITS api - http://www.lifl.fr/RD2P/JITS/Index) in file tests/jits/dictJits.txt To run the example, follow the steps: 1. go in the bin directory of STAN instalation: $cd bin 2. run the analysis using the predefined configuration in bin/config.xml (purse): $if_analyze -c purse -x ../tests/purseApp/classes The predefined configuration uses an already defined policy ( in /tests/purseApp/policy.txt). This policy declares as secret authentification attributes of class Purse (PIN, PUK, APIN). The predifined configuration can be found in the file bin/config.xml. Html files containing methods' signatures are generated, under /tests/purseApp/html_purse_dump directory. Annotated .class files are also generated under /tests/purseApp/annotated. The result of the analysis will be a dictionary, dictPurse.txt under tests/purse directory. The next step is to inspect this dictionary. 3. inspect the dictionary to see if any leaks of information were detected $if_inspectDico -d ../tests/purseApp/dictPurse.txt -p ../tests/purseApp/policy -x ../tests/purseApp/classes How to write a hand-annotation ------------------------------ The analyser allows adding hand-written annotations to the dictionary, using the -H option. The file specified by this option should have a predefined format : -------------format of hand-written annotations---------- java.lang.Math.sin(D)D [FlowAnnotation]0>4:16, java.lang.Float.floatToIntBits(F)I [FlowAnnotation]0>4:16, java.lang.System.gc()V [FlowAnnotation] ------------------end------------------------------------- The name of the method (package.method.signature) should be written on the first line, and the signature on the second line. The second line must begin with the string "[FlowAnnotation]" and must continue with the enumeration of links non-null in the signature of a method ( read http://www.lifl.fr/~ghindici/STAN/description.php to see the format of an annotation and the possible values of links). The non-null links are specified as follows: id_line>id_column:link. Elements must be separated by comma ",". Onboard lightweight verification -------------------------------- Results obtained offline, using the STAN tool, must be verified at loading time. To help the verification, .class files are annotated with methods signatures, and with some proof. The proof allows a linear verification of the bytecode. To annotate the .class files, don't forget to use the option -a/--annotate and to specify the output directory while analysing a set of classes with the if_analyze script. The resulting dictionary is not enough to annotate the .class files and it is not computed for this purpose. The .class files must be annotated during the analysis, when the proof is also computed. Encountered problems -------------------- Problems compiling using Ant were encountered while compiling on Unix platforms. If you get the message "...unable to find a javac compiler: com.sun.tools.javac.Main is not on the classpath. Perhaps JAVA_HOME does not point to the JDK", try to add the /lib/tools.jar, found under you jdk installation, to your classpath. We tested using Apache Ant version 1.6.5. Licence ------- Additional informations ----------------------- More information about STAN can be found at STAN web site: http://www.lifl.fr/~ghindici/STAN/ If you use STAN or if you have comments or bug reports, let us know! Don't hesitate to send an email to Dorina Ghindici at ghindici@lifl.fr