Inputs on Demand!
ISLa is a grammar-aware string constraint solver with its own specification language. With ISLa, it is possible to specify input constraints like "a variable has to be defined before it is used," "the `file name' block must be 100 bytes long," or "the number of columns in all CSV rows must be identical."
Building on modern constraint solvers, ISLa provides you with a unique flexibility to specify—and generate—the system inputs you need. ISLa can be used for precise fuzzing: Keep adding input specifications until you are satisfied with the number of inputs passing the tested system's parser. Furthermore, you can write ISLa specifications to carve out specific inputs for testing a particular program functionality.
Our running example is a simple "assignment language" consisting of strings such as
x := 1 ; y := x. As a first step towards using ISLa, we formalize this language as
a context-free grammar in BNF:
<start> ::= <stmt>
<stmt> ::= <assgn> | <assgn> " ; " <stmt>
<assgn> ::= <var> " := " <rhs>
<rhs> ::= <var> | <digit>
<var> ::= "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" |
"k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" |
"u" | "v" | "w" | "x" | "y" | "z"
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
After saving this grammar to a file, say, assgn.bnf, we can already generate inputs
from the assignment grammar using the ISLa command line interface:
> isla solve assgn.bnf
s := tThe following command creates 10 assignments:
> isla solve -n 10 assgn.bnf
a := 6 ; j := x
q := u
e := h ; o := l ; g := w
s := i
k := v ; d := m ; f := 1
n := y ; t := 5
z := 3 ; p := 7 ; b := 0
c := 2 ; r := 4
q := 8 ; l := 9
u := 0The setting -n -1 specifies that we want to generate an infinite number of inputs.
Since we did not choose an ISLa constraint, we additionally have to choose a value
for the -f flag. This setting determines the number of times an input element that
is not subject to any constraint (which is the case here) should be expanded. The final
line "UNSAT" means that after these 10 solutions, no further solution could be found.
If "UNSAT" is the first line output by the solver, it is likely that the given
constraint is unsatisfiable, i.e., there exists no solution of this constraint with
respect to the current grammar.
With ISLa, we can restrict the assignment language on-demand. For example, the ISLa
constraint <var> = "a" results in assignment sequences only containing "a" variables:
> isla solve /tmp/assgn.bnf -n 10 -f 1 --constraint '<var> = "a"'
a := 5 ; a := a ; a := 7
a := 6
a := a
a := 0 ; a := a ; a := a
a := a ; a := 1 ; a := 4
a := a ; a := 3 ; a := a
a := 8 ; a := 2
a := 9 ; a := a
a := a ; a := 9
a := a ; a := a💡 The setting
-f 1restricts the number of times that ILSa randomly instantiates unconstrained input elements to one time. Here, this affects the<digit>nonterminals: Without-f 1, we would see 10 different variants of the first input with variying numbers in the first and third assignment.
Or do we prefer assignments where all digits can be divided by 2 without remainder? No problem with ISLa:
> isla solve assgn.bnf -n 10 -f 1 -s 2 --constraint "str.to.int(<digit>) mod 2 = 0"
i := a ; x := 0 ; u := s
p := l ; m := 8 ; b := y
k := c ; t := d ; r := q
j := z
h := 0
e := 4
g := n ; v := f ; w := 4
o := o ; j := a ; c := 0
t := r ; k := 0 ; e := 0
k := t ; f := 8 ; e := 8💡 The
-sflag specifies how many results for a single query should be obtained from the SMT solver Z3. We limited this number to 2 (the default is 10—the same default value is used for the-fflag) to obtain a wider diversity of inputs within the first 10 results.
The constraints above talk over all <var> and <digit> grammar nonterminals in
any derivation tree derived from the assignment language grammar. In addition to such
simple constraints, ISLa allows to explicitly quantify over grammar elements using
the forall and exists keywords.
Assume that an interpreter for our assignment language rejects inputs where a variable is accessed that has not been previously assigned a value. This "definition-use" property, which is a semantic input property of the language, is expressed as follows:
forall <assgn> assgn_1:
exists <assgn> assgn_2: (
before(assgn_2, assgn_1) and
assgn_1.<rhs>.<var> = assgn_2.<var>)
Since this is a more lengthy constraint, let us save it in a file defuse.isla. The
following command line invocation uses this constraint:
> isla solve -n 10 -f 1 -s 1 assgn.bnf defuse.isla
q := 2 ; m := 1 ; c := 4
p := 8 ; o := 3 ; l := p
z := 7 ; p := 6 ; e := p
d := 5 ; a := d ; h := 9
s := 0 ; x := 0
k := 8
p := 4 ; r := p
p := 6 ; u := p
p := 5 ; v := p
p := 3 ; p := 5 ; w := pAs we can see, all right-hand side variables occur at the left-hand side of a prior assignment.
For more information on the command line interface, run isla -h. Each sub command
comes with its own help text; for example, isla solve -h provides details on how to
use the solve command.
You can also use the ISLa solver via its Python API:
from isla.solver import ISLaSolver
grammar = '''
<start> ::= <stmt>
<stmt> ::= <assgn> | <assgn> " ; " <stmt>
<assgn> ::= <var> " := " <rhs>
<rhs> ::= <var> | <digit>
<var> ::= "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" |
"k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" |
"u" | "v" | "w" | "x" | "y" | "z"
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
'''
constraint = """
forall <assgn> assgn_1:
exists <assgn> assgn_2: (
before(assgn_2, assgn_1) and
assgn_1.<rhs>.<var> = assgn_2.<var>)
"""
solver = ISLaSolver(
grammar=grammar,
formula=constraint,
max_number_free_instantiations=1, # -f
max_number_smt_instantiations=1, # -s
)
for _ in range(10):
print(solver.solve())An example output of the above program snippet is:
q := 7 ; m := 1 ; c := 8
p := 2 ; o := 2 ; l := p
z := 9 ; p := 4 ; e := p
d := 8 ; a := d ; h := 5
s := 0 ; x := 0
k := 7
p := 8 ; r := p
p := 9 ; u := p
p := 4 ; v := p
p := 2 ; p := 1 ; w := p
-
Our interactive ISLa tutorial, published as a part of the Fuzzing Book, provides an easily accessible introduction to the specification and generation of custom system inputs using ISLa.
-
The ISLa Documentation contains
- installation and usage instructions;
- further examples;
- the ISLa Language Specification, which precisely specifies the syntax and semantics of ISLa constraints. It also contains a list of supported default predicates;
- and a Developer's Guide to get started with ISLa's code.
-
We published a scientific paper on ISLa at ESEC/FSE 2022. The paper describes the ISLa language and solver more formally.
-
In the directory
src/isla_formalizations/, you find our specifications for the subject languages of our experimental evaluation. -
The files
run_eval_....fishare the scripts we used to collect and analyze our evaluation data. To analyze ISLa's current performance yourself, you can run the scripts with the-hargument to obtain some guidance on their parameters (the fish shell is required to use these scripts).
ISLa depends on Python 3.10 and the Python header files. To compile all of ISLa's dependencies, you need gcc, g++ make, and cmake. To check out the current ISLa version, git will be needed. Furthermore, python3.10-venv is required to run ISLearn in a virtual environment.
Additionally, for testing ISLa, clang and the csvlint executable are required (for
the Scriptsize-C and CSV case studies).
On Alpine Linux, all dependencies (but csvlint) can be installed using
apk add python3.10 python3.10-dev python3.10-venv gcc g++ make cmake git clangThe csvlint executable can be obtained from
https://github.com/Clever/csvlint/releases/download/v0.3.0/csvlint-v0.3.0-linux-amd64.tar.gz.
You obtain and unpack csvlint by running (in a Unix shell)
wget https://github.com/Clever/csvlint/releases/download/v0.3.0/csvlint-v0.3.0-linux-amd64.tar.gz -O /tmp/csvlint.tar.gz
tar xzf /tmp/csvlint.tar.gz -C /tmpThen, move the file /tmp/csvlint-v0.3.0-linux-amd64/csvlint to some location in your
PATH (e.g., /usr/bin).
If all external dependencies are available, a simple pip install isla-solver suffices.
We recommend installing ISLa inside a virtual environment (virtualenv):
python3.10 -m venv venv
source venv/bin/activate
pip install --upgrade pip
pip install isla-solverNow, the isla command should be available on the command line within the virtual
environment.
For testing ISLa without having to care about external dependencies like Python, we provide a Docker container, which already contains all dependencies.
First, pull and run the Docker container:
docker pull dsteinhoefel/isla:latest
docker run -it --name isla dsteinhoefel/islaYou should now have entered the container. Next, check out the ISLa repository, and update the requirements:
git clone https://github.com/rindPHI/isla.git
cd isla/Now, you can perform an editable installation of ISLa and run the ISLa tests:
pip install -e .[dev,test]
python3.10 -m pytest -n 16 testsISLearn is built locally as follows:
git clone https://github.com/rindPHI/isla.git
cd isla/
python3.10 -m venv venv
source venv/bin/activate
pip install --upgrade pip
pip install --upgrade build
python3 -m buildThen, you will find the built wheel (*.whl) in the dist/ directory.
For development, we recommend using ISLa inside a virtual environment (virtualenv). By thing the following steps in a standard shell (bash), one can run the ISLa tests:
git clone https://github.com/rindPHI/isla.git
cd isla/
python3.10 -m venv venv
source venv/bin/activate
pip install --upgrade pip
pip install -r requirements_test.txt
# Run tests
pip install -e .[dev,test]
python3 -m pytest -n 16 testsThen you can, for instance, run python3 tests/xml_demo.py inside the virtual environment.
See CHANGELOG.md.
Copyright © 2022 CISPA Helmholtz Center for Information Security.
The ISLa code and documentation was, unless otherwise indicated, authored by Dominic Steinhöfel.
ISLa is released under the GNU General Public License v3.0 (see COPYING).