Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. Research
  3. Data, Knowledge and Action
  4. Projects
  5. ArtForm

ArtForm

ArtForm is a concolic execution and testing tool for JavaScript code attached to web forms.

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.

Interface Analysis

ArtForm Manual Mode: Allows manual interaction with the page and trace recording.

Understanding and exploring web interfaces is useful for testing, web crawling and data extraction. We aim to analyse JavaScript code attached to web forms and generate tests which explore its behaviour.

  • Dynamic features of JavaScript and real-world code make static analysis difficult.
  • We use concolic analysis and perform a symbolic execution driven by concrete runs.
  • ArtForm is built on Artemis, a tool for automated testing of JavaScript applications.

ArtForm Poster

ArtForm Architecture

ArtForm Architecture: An instrumented version of WebKit records symbolic information which is used to generate new concrete inputs to test.

Interface Analyser

  • Chooses the entry-point.
  • Could be buttons, links, images or inputs and forms may cover the entire page.
  • ArtForm uses DIADEM for page analysis.

Test Driver

  • 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.

Symbolic Interpreter

  • Tracks both concrete and symbolic values.
  • Form inputs are initially symbolic variables and symbolic information is propagated as they are used.
  • Records the path taken and the symbolic branches observed.

Constraint Solver

  • 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.

Trace Classifier

  • Decides whether a trace was a successful submission or not.
  • Based on alerts, changes to the DOM and page loads.

Path Tree

  • Stores information about the previous runs.

Search Procedure

  • Chooses the next path to explore.
  • We are Investigating good search strategies to find interesting parts of the tree more quickly.

Example

Site: www.underwoods.co.uk/search.cfm

Search form for underwoods.co.uk

The execution tree for the underwoods.co.uk form.

Statistics
Symbolic branches explored: 629
Traces explored: 412
Successful submissions: 248
Failed submissions: 164
Constraints solved: 692

Legend
Dark green, numbered: Event handlers
Light blue, two children: Symbolic branches
Right/green edges: Condition is true, branch taken
Left/red edges: Condition is false, branch not taken
Green 'S': Successful submission
Red 'F': Failed submission
Purple 'U': Unreachable path (constraint was unsatisfiable)
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 source code.

Path Trace Report: Shows event handlers and functions called in the recorded trace. Coverage Report: Shows which lines in the JavaScript source were covered or contained symbolic information.

Principal Investigator

Michael Benedikt

People

Ben Spencer
Franck van Breugel

Share this:

See also

Back to Top