Skip to content

Update website to reflect new output #376

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Update website to reflect new output #376

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions docs/reference.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,9 @@ <h2>General options</h2>

<li><code>--num-unroll=&lt;num&gt;</code> &mdash; Specifies the number of times to unroll each loop. WP will unroll each loop 5 times by default.</code></li>

<li><code>--gdb-output=&lt;filename.gdb&gt;</code> &mdash; When WP results in SAT, outputs a <code>gdb</code> script to file <code>filename.gdb</code>. From within <code>gdb</code>, run <code>source filename.gdb</code> to set a breakpoint at the function given by <code>--func</code> and fill the appropriate registers with the values found in the countermodel. In the case WP returns UNSAT or UNKNOWN, no script will be outputted.</li>
<li><code>--gdb-output=&lt;filename.gdb&gt;</code> &mdash; When WP finds a countermodel, outputs a <code>gdb</code> script to file <code>filename.gdb</code>. From within <code>gdb</code>, run <code>source filename.gdb</code> to set a breakpoint at the function given by <code>--func</code> and fill the appropriate registers with the values found in the countermodel. In the case WP cannot falsify the property or returns UNKNOWN, no script will be outputted.</li>

<li><code>--bildb-output=&lt;filename.yml&gt;</code> &mdash; When WP results in SAT, outputs a BILDB initialization script to file <code>filename.yml</code>. This YAML file sets the registers and memory to the values found in the countermodel, allowing BILDB to follow the same execution trace. In the case the analysis returns UNSAT or UNKNOWN, no script will be outputted.</li>
<li><code>--bildb-output=&lt;filename.yml&gt;</code> &mdash; When WP finds a countermodel, outputs a BILDB initialization script to file <code>filename.yml</code>. This YAML file sets the registers and memory to the values found in the countermodel, allowing BILDB to follow the same execution trace. In the case the analysis cannot falsify the property or returns UNKNOWN, no script will be outputted.</li>

<li><code>--use-fun-input-regs</code> &mdash; At a function call site, uses all possible input registers as arguments to a function symbol generated for an output register. If this flag is not present, no registers will be used.</li>

Expand All @@ -59,7 +59,7 @@ <h2>General options</h2>
<li><code>--show=[bir|refuted-goals|paths|precond-internal|precond-smtlib]</code> &mdash; A list of details to print out from the analysis. Multiple options can be specified as a comma-separated list. For example: <code>--show=bir,refuted-goals</code>. The options are:
<ul>
<li><code>bir</code>: The code of the binary/binaries in BAP Intermediate Representation.</li>
<li><code>refuted-goals</code>: In the case WP results in SAT, a list of goals refuted in the model that contains their tagged names, their concrete values, and their Z3 representation.</li>
<li><code>refuted-goals</code>: In the case WP finds a countermodel, a list of goals refuted in the model that contains their tagged names, their concrete values, and their Z3 representation.</li>
<li><code>paths</code>: The execution path of the binary that results in a refuted goal. The path contains information about the jumps taken, their addresses, and the values of the registers at each jump. This option automatically prints out the refuted goals.</li>
<li><code>precond-smtlib</code>: The precondition printed out in Z3's SMT-LIB2 format.</li>
<li><code>precond-internal</code>: The precondition printed out in WP's internal format for the <code>Constr.t</code> type.</li>
Expand Down
37 changes: 19 additions & 18 deletions docs/tutorial.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -354,7 +354,7 @@ <h2>Tripping asserts</h2>
<p>Here we ask <code class="wp">wp</code> to try to trip an assert inside the <code>main</code> function of the program at <code>01/binary/main</code>. When we run this command, the relevant output comes at the end, which looks like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
ZF |-> 0x0
Expand All @@ -377,7 +377,7 @@ <h2>Tripping asserts</h2>
mem_mod = mem_orig
</pre>

<p>The first thing it says is <code>SAT!</code>, which means that CBAT was able to find a way to trip the assert.
<p>The first thing it says is <code>Property falsified. Counterexample found.</code>, which means that CBAT was able to find a way to trip the assert.

<p>Next, it says <code>Model</code>, after which it lists some information. There, you can see a bunch of registers on the left, and a bunch of values on the right (and a mention of memory at the bottom, which we can ignore for now).

Expand Down Expand Up @@ -653,7 +653,7 @@ <h2>4-Rooks</h2>
<p>After a moment, <code class="wp">wp</code> returns a result. At the end of the output, you should see something like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
ZF |-> 0x0
Expand Down Expand Up @@ -746,7 +746,7 @@ <h2>Find a Null Dereference</h2>
<p>If you run this, you'll see output that looks something like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
ZF |-> 0x0
Expand All @@ -770,7 +770,7 @@ <h2>Find a Null Dereference</h2>
malloc_ret_RAX016 |-> 0x0000000000000000
</pre>

<p>First, it says <code>SAT!</code>, indicating that it did in fact find a way to trigger the null dereference. Second, it gives us a <code>Model</code>, which shows us how to do it. Notice in particular the very last line:
<p>First, it says <code>Property falsified. Counterexample found.</code>, indicating that it did in fact find a way to trigger the null dereference. Second, it gives us a <code>Model</code>, which shows us how to do it. Notice in particular the very last line:

<pre>
malloc_ret_RAX016 |-> 0x0000000000000000
Expand Down Expand Up @@ -812,10 +812,10 @@ <h2>Find a Null Dereference</h2>
Evaluating precondition.
Checking precondition with Z3.

UNSAT!
No counterexample found.
</pre>

<p>This time, <code class="wp">wp</code> says <code>UNSAT</code>, which is the opposite of <code>SAT</code>. In other words, <code class="wp">wp</code> has found that there are no null dereferences in <code>main</code>. And that is correct. There is indeed no possible way to dereference a null pointer in this version of the program, which <code class="wp">wp</code> confirms.
<p>This time, <code class="wp">wp</code> says <code>No counterexample found.</code>. In other words, <code class="wp">wp</code> has found that there are no null dereferences in <code>main</code>. And that is correct. There is indeed no possible way to dereference a null pointer in this version of the program, which <code class="wp">wp</code> confirms.

</section>

Expand Down Expand Up @@ -907,7 +907,7 @@ <h3>Example: Verifying an optimization</h3>
Evaluating precondition.
Checking precondition with Z3.

UNSAT!
No counterexample found.
</pre>

<p>What this means is that <code class="wp">wp</code> was not able to find a way to make these two function produce different outputs. And remember, <code class="wp">wp</code> does a logical check, so this is telling us that (up to our simplifying assumptions) it is logically impossible for these two functions to produce different outputs.
Expand Down Expand Up @@ -1091,7 +1091,7 @@ <h2>Comparing Function Calls</h2>
<p>The output looks something like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
ZF |-> 0x0
Expand All @@ -1114,7 +1114,7 @@ <h2>Comparing Function Calls</h2>
mem_mod = mem_orig
</pre>

<p>This says <code>SAT</code>, which means <code class="wp">wp</code> did indeed find a way to make the older and patched versions of these functions make different function calls.
<p>This says <code>Property falsified. Counterexample found</code>, which means <code class="wp">wp</code> did indeed find a way to make the older and patched versions of these functions make different function calls.

<p>Note the <code>Model</code>, which tells us that this violation occurs when <code>RDI</code> is set to <code>0x01</code>. So if the value <code>0x01</code> is stored in <code>RDI</code> when these functions start, then the second version of the function will call fewer functions than the first version.

Expand Down Expand Up @@ -1158,7 +1158,7 @@ <h2>Comparing Function Calls</h2>
<p>Then <code class="wp">wp</code> prints output that looks something like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
ZF |-> 0x0
Expand Down Expand Up @@ -1274,7 +1274,8 @@ <h2>Custom Postcondition (One Binary)</h2>
<p>When <code class="wp">wp</code> runs this, it will try to falsify this property. That is, it will explore all logical possibilities (up to our simplifying assumptions), and find a way to make our <code>main</code> function put something other than <code>7</code> in <code>RAX</code>.

<ul>
<li>If <code class="wp">wp</code> can find a way to falsify our property, it will return <code>SAT</code> and provide an example of how to make <code>main</code> produce a value other than <code>7</code>.</li>
<li>If <code class="wp">wp</code> can find a way to falsify our property, it will return <code>Property falsified.
Counterexample found</code> and provide an example of how to make <code>main</code> produce a value other than <code>7</code>.</li>
<li>If it cannot falsify our property, it will return <code>UNSAT</code>, and that means the property holds. It means that <code>RAX</code> does indeed always contain the 64-bit number 7 at the end of our <code>main</code> function's execution.</li>
</ul>

Expand All @@ -1284,7 +1285,7 @@ <h2>Custom Postcondition (One Binary)</h2>
Evaluating precondition.
Checking precondition with Z3.

UNSAT!
No counterexample found.
</pre>

<p>So, in this case, <code class="wp">wp</code> could not find a way to falsify this property, and hence the property holds. And indeed, that makes sense, because as we can see from the code, our function always returns the number <code>7</code>.
Expand All @@ -1308,7 +1309,7 @@ <h2>Custom Postcondition (One Binary)</h2>
<p>This time, <code class="wp">wp</code> outputs something that looks like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
RSP |-> 0x000000003f800081
Expand All @@ -1330,7 +1331,7 @@ <h2>Custom Postcondition (One Binary)</h2>
Z3 Expression: = #x0000000000000007 #x0000000000000003
</pre>

<p>This time, <code class="wp">wp</code> comes back with <code>SAT</code>, meaning that it could find a way to falsify our assertion, and it shows us how to do it. In the <code>model</code>, most of the values are zero, which makes sense. Since our <code>main</code> function always returns <code>7</code>, the registers can start with pretty much any values (or no values), and <code>main</code> will not produce <code>3</code> in <code>RAX</code>.
<p>This time, <code class="wp">wp</code> comes back with <code>Property falsified. Counterexample found</code>, meaning that it could find a way to falsify our assertion, and it shows us how to do it. In the <code>model</code>, most of the values are zero, which makes sense. Since our <code>main</code> function always returns <code>7</code>, the registers can start with pretty much any values (or no values), and <code>main</code> will not produce <code>3</code> in <code>RAX</code>.

</section>

Expand Down Expand Up @@ -1367,7 +1368,7 @@ <h2>Custom Pre and Postcondition (One Binary)</h2>
<p>When you run that, you'll see that <code class="wp">wp</code> produces output that looks something like this:

<pre>
SAT!
Property falsified. Counterexample found.

Model:
ZF |-> 0x0
Expand Down Expand Up @@ -1426,7 +1427,7 @@ <h2>Custom Pre and Postcondition (One Binary)</h2>
Evaluating precondition.
Checking precondition with Z3.

UNSAT!
No counterexample found.
</pre>

<p>In other words, <code class="wp">wp</code> was not able to find a way to falsify our assertions, and hence our assertions hold.
Expand Down Expand Up @@ -1512,7 +1513,7 @@ <h2>Custom Postcondition (Two Binaries)</h2>
Evaluating precondition.
Checking precondition with Z3.

UNSAT!
No counterexample found.
</pre>

<p>In other words, <code class="wp">wp</code> could not find a way to falsify our assertion. Hence, the property we've asserted here holds. <code>RAX</code> in the original and the modified program will indeed always be equal.
Expand Down