ArtForm is the name for the form- and interface-analysis modes of Artemis.
ArtForm uses concolic execution to explore different execution paths of JavaScript code attached to web forms.
For more information, see: www.cs.ox.ac.uk/projects/ArtForm/
A demo screencast is available at: www.cs.ox.ac.uk/projects/ArtForm/demo/
The main installation instructions already include everything required for ArtForm.
Manual mode is used to manually interact with a web page and see what information is recorded by our symbolic tracing infrastructure.
As an example, try:
artemis --major-mode manual --path-trace-report html --coverage-report html http://www.example.com
Some small synthetic examples are offered when just running:
artemis --major-mode manual
The concolic mode uses concolic execution to automatically explore the JavaScript code attached to web forms.
An example call mgiht be:
artemis --major-mode concolic --concolic-tree-output final-overview -i 0 --concolic-event-sequences simple --concolic-event-handler-report --concolic-search-procedure selector --concolic-selection-procedure "round-robin(avoid-unsat:random)" --concolic-selection-budget 50 --coverage-report html --concolic-button "//xpath/to/the/submit/button" http://www.example.com
Here we have provided the URL of the page to analyse, and an XPath expression to identify the form's submit button. ArtForm will load the page, and fill each form field before clicking the submit button. This forms a single iteration or symbolic trace. Whenever a form input value is used to control the JavaScript execution (e.g. in form validation code), ArtForm's concolic execution will generate new input values to excercise that code path and test them on a subsequent iteration.
ArtForm can also run in an "advice server" mode, where the browser can be controlled externally via a JSON API. The client sends browser commands and can control the concolic execution - recording symbolic traces and requesting new suggested values.
For full details on the advice API, see the server mode documentation, and concolic execution in advice mode.
An example call might be:
artemis --major-mode server --analysis-server-port 8008 --analysis-server-log --coverage-report html --analysis-server-debug-view
At which point the API commands can be sent:
$ curl -w "\n" --data '{"command":"pageload","url":"http://www.example.com"}' localhost:8008
{ "pageload" : "done", "url" : "http://www.example.com/" }
$ curl -w "\n" --data '{"command":"element","element":"//h1"}' localhost:8008
{ "elements" : [ "<h1>Example Domain</h1>" ] }
ArtForm is implemented as a set of new modes for the original Artemis tool. There are significant updates and changes throughout Artemis, but the key new components are as follows:
- The main controlling code (called a
Runtime) for each of the new modes: concolic, concolic standalone (without forms support), manual, and advice server. - The symbolic interpreter, and symbolic expressions
- The creation of fresh symbolic values: directly (see
globalFuncArtemisInput*), and from forms (this is the code generator for the relevant JS DOM API, search forARTEMISorSymbolicInputElement; the code is generated from modified IDL files here) - Input simulation
- Form modelling
- The JSON server which forms the API for advice mode
- The path trace reporting
- The coverage report (from the original Artemis)
- The main concolic advice infrastructure, including:
- Automated test suites for concolic and server modes, and various parts of the symbolic infrastructure
- A proxy which rewrites JavaScript code into an un-minified form
Further documentation of the low-level changes within WebKit is in the docs directory (or online). In particular, see Concolic Testing Framework, Concolic infrastructure test mode, Server Mode, and Server Mode - Concolic Advice.