tutorial.html from CQual at Krugle

Show tutorial.html syntax highlighted

<html>
<head>
<title>A Brief CQUAL Tutorial</title>
<style type"/text.css"><!--
.smallcap { font-variant: small-caps }
--></style>
</head>

<body bgcolor="white">
<h1>A Brief <span class=smallcap>Cqual</span> Tutorial</h1>

<p>
Below we present a small example showing how to use the web-based
version of <span class=smallcap>Cqual</span> to find a potential
format-string vulnerability in a C program.  This tutorial is
extracted from the documentation distributed with the source code.

<p>
Consider the following small example program:<br>
<pre>
char *getenv(const char *name);
int printf(const char *fmt, ...);

int main(void)
{
  char *s, *t;
  s = getenv("LD_LIBRARY_PATH");
  t = s;
  printf(t);
}
</pre>

<p>
This program reads the value of <tt>LD_LIBRARY_PATH</tt> from the
environment and passes it to <tt>printf</tt> as a format string.  If
the user can control the environment in which this program is run,
then this program may have a format-string vulnerability.  For
example, if the user sets <tt>LD_LIBRARY_PATH</tt> to a large sequence
of <tt>%s</tt>'s, the program will likely seg fault.

<p>
By default <span class=smallcap>Cqual</span> assumes nothing about the
behavior of your program.  In order to start checking for bugs, we
need to annotate the program with extra <i>type qualifiers</i>.  For
this example we will use two qualifiers.  We will annotate untrusted
strings as <tt>$tainted</tt>, and we will require that <tt>printf</tt>
take <tt>$untainted</tt> data:
<pre>
<font color=red>$tainted</font> char *getenv(const char *name);
int printf(<font color=green>$untainted</font> const char *fmt, ...);

int main(void)
{
  char *s, *t;
  s = getenv("LD_LIBRARY_PATH");
  t = s;
  printf(t);
}
</pre>

<p>
In <span class=smallcap>Cqual</span> all user-defined qualifiers,
which we will refer to as <i>constant qualifiers</i>, begin with
dollar signs.  Notice that we only need to annotate <tt>getenv</tt>
and <tt>printf</tt> with type qualifiers.  For this example <span
class=smallcap>Cqual</span> will infer that <tt>s</tt> and <tt>t</tt>
must also be <tt>$tainted</tt>, and hence will signal a type error:
<tt>$tainted</tt> data is being passed to <tt>printf</tt>, which
requires <tt>$untainted</tt> data.  The presence of a type error
indicates a potential format-string vulnerability.

<h2>Running <span class=smallcap>Cqual</span></h2>

<p>
Use the web interface to analyze this program, listed as ``Tainting:
Small Example'' in the drop-down menu.  <span
class=smallcap>Cqual</span> analyzes the file and brings up a window
listing the input files and the analysis results.  In this case,
<span class=smallcap>Cqual</span> complains
<pre>
taint.c:9
type of actual argument 1 doesn't match type of formal
unsatisfiable qualifier constraint $tainted &lt;= $untainted
</pre>
Error messages are linked to the position in the file where the error
was generated.  You can also click on a file name to jump to the top
of the file.

<p>
If you click on the error message link you will see a marked-up
display of <tt>taint.c</tt>, the input file.  Identifiers are colored
according to their inferred qualifiers.  In the web version of <span
class=smallcap>Cqual</span>, <tt>$tainted</tt> identifiers are colored
red, <tt>$untainted</tt> identifiers are colored green, and
identifiers that may contribute to a type error are colored purple.

<p>
Each marked-up identifier is also a hyperlink.  Clicking on an
identifier will show you the type of the identifier, fully annotated
with qualifiers.  For example, clicking on <tt>t</tt> should display
<pre>
t: t ptr (t' ptr (t'' char))
</pre>
in the bottom frame.

<p>
The name of the identifier is shown to the left of the colon, and its
inferred type is shown to the right of the colon.  Here <tt>t</tt> has
the type pointer to pointer to character.  (We will explain the extra
level of <tt>ptr</tt> below.)  Notice that <span
class=smallcap>Cqual</span> writes types from left-to-right using
<tt>ptr</tt> as a type constructor.

<p>
The three hyperlinked names in the type are <i>qualifier
variables</i>.  In this case the qualifier variable <tt>t''</tt> is
colored purple because it has been inferred to be both
<tt>$tainted</tt> and <tt>$untainted</tt>, an error.

<p>
Clicking on a qualifier variable will show you the inferred value of
the qualifier variable and the shortest path on which it was inferred
to have its value.  For example, if you click on <tt>t''</tt>, you
should see the following result:
<pre>
t'':  $tainted $untainted

$tainted &lt;= getenv_ret'
         &lt;= s''
         &lt;= t''
         &lt;= printf_arg0'
         &lt;= $untainted
</pre>

<p>
The first line tells us that <tt>t''</tt> is both <tt>$tainted</tt>
and <tt>$untainted</tt>, an error.  The remaining lines show us an
erroneous path.  We see that <tt>t''</tt> was tainted from
<tt>s''</tt>, which was tainted from the return type of
<tt>getenv</tt>.  We also see that the error arises because
<tt>t''</tt> taints the parameter to <tt>printf</tt>, which must be
untainted.

<p>
Clicking on a <tt>&lt;=</tt> will jump to the source location where
that constraint was generated.  Clicking an a qualifier we compute the
shortest path by which that qualifier was inferred to have its value.

<h2><i>L</i>-values and <i>R</i>-values</h2>

<p>
In C there is an important distinction between <i>l</i>-values, which
correspond to memory locations, and <i>r</i>-values, which are
ordinary values like integers.  In the C type system, <i>l</i>-values
and <i>r</i>-values are given the same type.  For example, consider
the following code:
<pre>
int x;
x = ...;
... = x;
</pre>

<p>
The first line declares that <tt>x</tt> is a location containing an
integer.  On the second line <tt>x</tt> is used as an <i>l</i>-value:
it appears on the left-hand side of an assignment, meaning that the
location corresponding to <tt>x</tt> should be updated.  On the third
line <tt>x</tt> is used as an <i>r</i>-value.  Here when we use
<tt>x</tt> as an <i>r</i>-value we are not referring to the location
<tt>x</tt>, but to <tt>x</tt>'s contents.  In the C type system,
<tt>x</tt> is given the type <tt>int</tt> in both places, and the
syntax distinguishes integers that are <i>l</i>-values from integers
that are <i>r</i>-values.

<p>
<span class=smallcap>Cqual</span> uses a slightly different approach
in which the types distinguish <i>l</i>-values and <i>r</i>-values.
In <span class=smallcap>Cqual</span>, <tt>x</tt> is given the type
<tt>ptr(int)</tt>, meaning that the name <tt>x</tt> is a location
containing an integer.  When <tt>x</tt> is used as an <i>l</i>-value
its type stays the same---in <span class=smallcap>Cqual</span>, the
left-hand side of an assignment is always a <tt>ptr</tt> type.  When
<tt>x</tt> is used as an <i>r</i>-value the outermost <tt>ptr</tt> is
removed, i.e., <tt>x</tt> as an <i>r</i>-value has the type
<tt>int</tt>.

<p>
In more concrete terms, if you click on an identifier <tt>a</tt> that
can be used as an <i>l</i>-value you will see <tt>a</tt>'s type as an
<i>l</i>-value, i.e., with an extra <tt>ptr</tt> at the top-level.
For most purposes you can safely ignore this extra level of
indirection.

</body> </html>
See more files for this project here