This is a collaboration with Casper Svenning Jensen and Anders
Møller, Aarhus University.
Our prototype tool is available on GitHub. Please
contact Ben Spencer for support installing and using it.
code attached to web forms and generate tests which explore its behaviour.
- We use concolic analysis and perform a symbolic execution driven by concrete runs.
- ArtForm is built on Artemis, a tool for automated testing
- Chooses the entry-point.
- Could be buttons, links, images or inputs and forms may cover the entire page.
- ArtForm uses DIADEM for page analysis.
- Loads the test page with no saved state.
- Injects the given inputs into the form.
- Simulates real click on submit button.
Instrumented WebKit Browser
- Controls all code execution and events.
- Allows access to the DOM implementation and page information.
- Tracks both concrete and symbolic values.
- Form inputs are initially symbolic variables and symbolic information is propagated as they
- Records the path taken and the symbolic branches observed.
- Solves the path constraint to generate the next input values to test.
- Translates our internal constraints to input for a third-party solver.
- ArtForm uses CVC4.
- Decides whether a trace was a successful submission or not.
- Based on alerts, changes to the DOM and page loads.
- Stores information about the previous runs.
- Chooses the next path to explore.
- We are Investigating good search strategies to find interesting parts of the tree more quickly.
Symbolic branches explored: 629
Traces explored: 412
Successful submissions: 248
Failed submissions: 164
Constraints solved: 692
Dark green, numbered: Event handlers
Light blue, two children:
Right/green edges: Condition is true, branch taken
Left/red edges: Condition is false, branch
Green 'S': Successful submission
Red 'F': Failed submission
Purple 'U': Unreachable path (constraint
Orange '!': Alert message
Light green 'L': New page loaded
Full execution tree (2.4MB png)
Page Analysis Tools
As well as our main analysis, we have developed some tools to help manual analysis of web forms and their validation code.
Manual interactions with a form are recorded as both concrete and symbolic traces, which are linked to the original page