2 \page other_documentation Other Documentation
6 We document two programs that try to achieve formal guarantees of the
7 absence of specific problems: CBMC and SATABS. The algorithms
8 implemented by CBMC and SATABS are complementary, and often, one tool is
9 able to solve a problem that the other cannot solve.
11 Both CBMC and SATABS are verification tools for ANSI-C/C++ programs.
12 They verify array bounds (buffer overflows), pointer safety, exceptions
13 and user-specified assertions. Both tools model integer arithmetic
14 accurately, and are able to reason about machine-level artifacts such as
15 integer overflow. CBMC and SATABS are therefore able to detect a class
16 of bugs that has so far gone unnoticed by many other verification tools.
17 This manual also covers some variants of CBMC, which includes HW-CBMC
19 \ref man_hard-soft-introduction "hardware/software co-verification".
21 ## Automatic Program Verification with SATABS
23 In many cases, lightweight properties such as array bounds do not rely
24 on the entire program. A large fraction of the program is *irrelevant*
25 to the property. SATABS exploits this observation and computes an
26 *abstraction* of the program in order to handle large amounts of code.
28 In order to use SATABS it is not necessary to understand the abstraction
29 refinement process. For the interested reader, a high-level introduction
30 to abstraction refinement is provided
31 \ref man_satabs-overview "here".
33 \ref man_satabs-tutorials "tutorials on how to use SATABS".
35 Just as CBMC, SATABS attempts to build counterexamples that refute the
36 property. If such a counterexample is found, it is presented to the
37 engineer to facilitate localization and repair of the program.
39 \subsection man_install-satabs Installing SATABS
43 SATABS is available for Windows, i86 Linux, and MacOS X. SATABS requires
44 a code pre-processing environment including a suitable preprocessor
45 and a set of header files.
47 1. **Linux:** the preprocessor and the header files typically come with
48 a package called *gcc*, which must be installed prior to the
49 installation of SATABS.
50 2. **Windows:** The Windows version of SATABS requires the preprocessor
51 `cl.exe`, which is part of Visual Studio (including the free [Visual
53 Express](http://msdn.microsoft.com/vstudio/express/visualc/)).
54 3. **MacOS:** Install Xcode command line tools: run
55 `xcode-select --install` prior to installing SATABS.
57 Important note for Windows users: Visual Studio's `cl.exe` relies on a
58 complex set of environment variables to identify the target architecture
59 and the directories that contain the header files. You must run SATABS
60 from within the *Visual Studio Command Prompt*.
62 Note that the distribution files for the [Eclipse
63 plugin](installation-plugin.shtml) include the command-line tools.
64 Therefore, if you intend to run SATABS exclusively within Eclipse, you
65 can skip the installation of the command-line tools. However, you still
66 have to install the compiler environment as described above.
68 ### Choosing and Installing a Model Checker
70 You need to install a Model Checker in order to be able to run SATABS.
71 You can choose between following alternatives:
73 - **Cadence SMV**. Available from http://www.kenmcmil.com/smv.html.
74 Cadence SMV is a commercial model checker. The free version that is
75 available on the homepage above must not be used for commercial
76 purposes (read the license agreement thoroughly before you download
77 the tool). The documentation for SMV can be found in the directory
78 where you unzip/untar SMV under ./smv/doc/smv/. Read the
79 installation instructions carefully. The Linux/MacOS versions
80 require setting environment variables. You must add add the
81 directory containing the `smv` binary (located in ./smv/bin/,
82 relative to the path where you unpacked it) to your `PATH`
83 environment variable. SATABS uses Cadence SMV by default.
85 - **NuSMV**. Available from http://nusmv.irst.itc.it/. NuSMV is the
86 open source alternative to Cadence SMV. Installation instructions
87 and documentation can be found on the NuSMV homepage. The directory
88 containing the NuSMV binary should be added to your `PATH`
89 environment variable. Use the option
93 to instruct SATABS to use NuSMV.
95 - **BOPPO**. Available from http://www.cprover.org/boppo/. BOPPO is
96 a model checker which uses SAT-solving algorithms. BOPPO relies on a
97 built-in SAT solver and Quantor, a solver for quantified boolean
98 formulas which is currently bundled with BOPPO, but also available
99 separately from <http://fmv.jku.at/quantor/>. We recommend to add
100 the directories containing both tools to your `PATH` environment
101 variable. Use the option
105 when you call SATABS and want it to use BOPPO instead of SMV.
107 - **BOOM**. Available from http://www.cprover.org/boom/. Boom has a
108 number of unique features, including the verification of programs
109 with unbounded thread creation.
111 ### Installing SATABS
113 1. Download SATABS for your operating system. The binaries are
114 available from <http://www.cprover.org/satabs/>.
115 2. Unzip/untar the archive into a directory of your choice. We
116 recommend to add this directory to your `PATH` environment variable.
118 Now you can execute SATABS. Try running SATABS on the small examples
119 presented in the \ref man_satabs-tutorials "SATABS tutorial". If you use
120 the Cadence SMV model checker, the only command line arguments you have
121 to specify are the names of the files that contain your program.
125 We provide a graphical user interface to CBMC and SATABS, which is
126 realized as a plugin to the Eclipse framework. Eclipse is available at
127 http://www.eclipse.org. We do not provide installation instructions for
128 Eclipse (basically, you only have to download the current version and
129 extract the files to your hard-disk) and assume that you have already
130 installed the current version.
132 CBMC and SATABS have their own requirements. As an example, both CBMC
133 and SATABS require a suitable preprocessor and a set of header files.
134 As first step, you should therefore follow the installation instructions
135 for \ref man_install-cbmc "CBMC" and \ref man_install-satabs "SATABS".
137 Important note for Windows users: Visual Studio's `cl.exe` relies on a
138 complex set of environment variables to identify the target architecture
139 and the directories that contain the header files. You must run Eclipse
140 from within the *Visual Studio Command Prompt*.
142 \section man_satabs SATABS---Predicate Abstraction with SAT
144 \subsection man_satabs-overview Overview
146 This section describes SATABS from the point of view of the user. To
147 learn about the technology implemented in SATABS, read
148 \ref man_satabs-background "this".
150 We assume you have already installed SATABS and the necessary support
151 files on your system. If not so, please follow
152 \ref man_install-satabs "these instructions".
154 While users of SATABS almost never have to be concerned about the
155 underlying refinement abstraction algorithms, understanding the classes
156 of properties that can be verified is crucial. Predicate abstraction is
157 most effective when applied to *control-flow dominated properties*. As
158 an example, reconsider the following program (lock-example-fixed.c):
179 unsigned got_lock = 0;
185 /* critical section */
198 The two assertions in the program model that the functions `lock()` and
199 `unlock()` are called in the right order. Note that the value of `times`
200 is chosen non-deterministically and is not bounded. The program has no
201 run-time bound, and thus, unwinding the code with CBMC will never
204 ### Working with Claims
206 The two assertions will give rise to two *properties*. Each property is
207 associated to a specific line of code, i.e., a property is violated when
208 some condition can become false at the corresponding program location.
209 SATABS will generate a list of all properties for the programs as
212 satabs lock-example-fixed.c --show-properties
214 SATABS will list two properties; each property corresponds to one of the
215 two assertions. We can use SATABS to verify both properties as follows:
217 satabs lock-example-fixed.c
219 SATABS will conclude the verification successfully, that is, both
220 assertions hold for execution traces of any length.
222 By default, SATABS attempts to verify all properties at once. A single
223 property can be verified (or refuted) by using the `--property id`
224 option of SATABS, where `id` denotes the identifier of the property in
225 the list obtained by calling SATABS with the `--show-properties` flag.
226 Whenever a property is violated, SATABS reports a feasible path that
227 leads to a state in which the condition that corresponds to the violated
228 property evaluates to false.
230 \subsection man_satabs-libraries Programs that use Libraries
232 SATABS cannot check programs that use functions that are only available
233 in binary (compiled) form (this restriction is not imposed by the
234 verification algorithms that are used by SATABS – they also work on
235 assembly code). The reason is simply that so far no assembly language
236 frontend is available for SATABS. At the moment, (library) functions for
237 which no C source code is available have to be replaced by stubs. The
238 usage of stubs and harnesses (as known from unit testing) also allows to
239 check more complicated properties (like, for example, whether function
240 `fopen` is always called before `fclose`). This technique is explained
241 in detail in the \ref man_satabs-tutorials "SATABS tutorials".
243 \subsection man_satabs-unit-test Unit Testing with SATABS
245 The example presented \ref man_satabs-tutorial-driver "here" is
246 obviously a toy example and can hardly be used to convince your project
247 manager to use static verification in your next project. Even though we
248 recommend to use formal verification and specification already in the
249 early phases of your project, the sad truth is that in most projects
250 verification (of any kind) is still pushed to the very end of the
251 development cycle. Therefore, this section is dedicated to the
252 verification of legacy code. However, the techniques presented here can
253 also be used for *unit testing*.
255 Unit testing is used in most software development projects, and static
256 verification with SATABS can be very well combined with this technique.
257 Unit testing relies on a number test cases that yield the desired code
258 coverage. Such test cases are implemented by a software testing engineer
259 in terms of a test harness (aka test driver) and a set of function
260 stubs. Typically, a slight modification to the test harness allows it to
261 be used with SATABS. Replacing the explicit input values with
262 non-deterministic inputs (as explained in
263 \ref man_satabs-tutorial-aeon "here" and
264 \ref man_satabs-tutorial-driver "here")) guarantees that SATABS will try
265 to achieve **full** path and state coverage (due to the fact that
266 predicate abstraction implicitly detects equivalence classes). However,
267 it is not guaranteed that SATABS terminates in all cases. Keep in mind
268 that you must not make any assumptions about the validity of the
269 properties if SATABS did not run to completion!
273 - [Model Checking Concurrent Linux Device
274 Drivers](http://www.kroening.com/publications/view-publications-wbwk2007.html)
275 - [SATABS: SAT-based Predicate Abstraction for
276 ANSI-C](http://www-2.cs.cmu.edu/~svc/papers/view-publications-cksy2005.html)
277 - [Predicate Abstraction of ANSI-C Programs using
278 SAT](http://www-2.cs.cmu.edu/~svc/papers/view-publications-cksy2004.html)
280 \subsection man_satabs-background Background
282 ### Sound Abstractions
284 This section provides background information on how SATABS operates.
285 Even for very trivial C programs it is impossible to exhaustively
286 examine their state space (which is potentially unbounded). However, not
287 all details in a C program necessarily contribute to a bug, so it may be
288 sufficient to only examine those parts of the program that are somehow
291 In practice, many static verification tools (such as `lint`) try to
292 achieve this goal by applying heuristics. This approach comes at a cost:
293 bugs might be overlooked because the heuristics do not cover all
294 relevant aspects of the program. Therefore, the conclusion that a
295 program is correct whenever such a static verification tool is unable to
296 find an error is invalid.
298 \image html cegar-1.png "CEGAR Loop"
300 A more sophisticated approach that has been very successful recently is
301 to generate a *sound* abstraction of the original program. In this
302 context, *soundness* refers to the fact that the abstract program
303 contains (at least) all relevant behaviors (i.e., bugs) that are present
304 in the original program. In the Figure above, the first component strips
305 details from the original program. The number of possible behaviors
306 increases as the number of details in the abstract program decreases.
307 Intuitively, the reason is that whenever the model checking tool lacks
308 the information that is necessary to make an accurate decision on
309 whether a branch of an control flow statement can be taken or not, both
310 branches have to be considered.
312 In the resulting *abstract program*, a set of concrete states is
313 subsumed by means of a single abstract state. Consider the following
318 The concrete states *x*~1~ and *x*~2~ are mapped to an abstract state
319 *X*, and similarly *Y* subsumes *y*~1~ and *y*~2~. However, all
320 transitions that are possible in the concrete program are also possible
321 in the abstract model. The abstract transition *X* → *Y* summarizes the
322 concrete transitions *x*~1~ → *y*~1~ and *x*~1~ → *x*~1~, and *Y* → *X*
323 corresponds to *x*~1~ → *x*~2~. The behavior *X* → *Y* → *X* is feasible
324 in the original program, because it maps to *x*~1~ → *x*~1~ → *x*~2~.
325 However, *Y* → *X* → *Y* is feasible only in the abstract model.
327 ### Spurious Counterexamples
329 The consequence is that the model checker (component number two in the
330 figure above) possibly reports a *spurious* counterexample. We call a
331 counterexample spurious whenever it is feasible in the current abstract
332 model but not in the original program. However, whenever the model
333 checker is unable to find an execution trace that violates the given
334 property, we can conclude that there is no such trace in the original
337 The feasibility of counterexamples is checked by *symbolic simulation*
338 (performed by component three in the figure above). If the
339 counterexample is indeed feasible, SATABS found a bug in the original
340 program and reports it to the user.
342 ### Automatic Refinement
344 On the other hand, infeasible counterexamples (that originate from
345 abstract behaviors that result from the omission of details and are not
346 present in the original program) are never reported to the user.
347 Instead, the information is used in order to refine the abstraction such
348 that the spurious counterexample is not part of the refined model
349 anymore. For instance, the reason for the infeasibility of *Y* → *X* →
350 *Y* is that neither *y*~1~ nor *x*~1~ can be reached from *x*~2~.
351 Therefore, the abstraction can be refined by partitioning *X*.
353 The refinement steps can be illustrated as follows:
355 
357 The first step (1) is to generate a very coarse abstraction with a very
358 small state space. This abstraction is then successively refined (2, 3,
359 ...) until either a feasible counterexample is found or the abstract
360 program is detailed enough to show that there is no path that leads to a
361 violation of the given property. The problem is that this point is not
362 necessarily reached for every input program, i.e., it is possible that
363 the the abstraction refinement loop never terminates. Therefore, SATABS
364 allows to specify an upper bound for the number of iterations.
366 When this upper bound is reached and no counterexample was found, this
367 does not necessarily mean that there is none. In this case, you cannot
368 make any conclusions at all with respect to the correctness of the input
371 \subsection man_satabs-tutorials Tutorials
373 We provide an introduction to model checking "real" C programs with
374 SATABS using two small examples.
376 \subsubsection man_satabs-tutorial-driver Reference Counting in Linux Device Drivers
378 Microsoft's [SLAM](http://research.microsoft.com/SLAM) toolkit has been
379 successfully used to find bugs in Windows device drivers. SLAM
380 automatically verifies device driver whether a device driver adheres to
381 a set of specifications. SLAM provides a test harness for device drivers
382 that calls the device driver dispatch routines in a non-deterministic
383 order. Therefore, the Model Checker examines all combinations of calls.
384 Motivated by the success this approach, we provide a toy example based
385 on Linux device drivers. For a more complete approach to the
386 verification of Linux device drivers, consider
387 [DDVerify](http://www.cprover.org/ddverify/).
389 Dynamically loadable modules enable the Linux Kernel to load device
390 drivers on demand and to release them when they are not needed anymore.
391 When a device driver is registered, the kernel provides a major number
392 that is used to uniquely identify the device driver. The corresponding
393 device can be accessed through special files in the filesystem; by
394 convention, they are located in the `/dev` directory. If a process
395 accesses a device file the kernel calls the corresponding `open`, `read`
396 and `write` functions of the device driver. Since a driver must not be
397 released by the kernel as long as it is used by at least one process,
398 the device driver must maintain a usage counter (in more recent Linux
399 kernels, this is done automatically, however, drivers that must maintain
400 backward compatibility have to adjust this counter).
402 We provide a skeleton of such a driver. Download the files
403 assets/spec.c, assets/driver.c, assets/driver.h, assets/kdev_t.h, and
406 The driver contains following functions:
408 1. `register_chrdev`: (in assets/spec.c) Registers a character device.
409 In our implementation, the function sets the variable `usecount` to
410 zero and returns a major number for this device (a constant, if the
411 user provides 0 as argument for the major number, and the value
412 specified by the user otherwise).
416 int register_chrdev (unsigned int major, const char* name)
424 2. `unregister_chrdev`: (in assets/spec.c) Unregisters a character
425 device. This function asserts that the device is not used by any
426 process anymore (we use the macro `MOD_IN_USE` to check this).
428 int unregister_chrdev (unsigned int major, const char* name)
438 3. `dummy_open`: (in assets/driver.c) This function increases the
439 `usecount`. If the device is locked by some other process
440 `dummy_open` returns -1. Otherwise it locks the device for the
443 4. `dummy_read`: (in assets/driver.c) This function "simulates" a read
444 access to the device. In fact it does nothing, since we are
445 currently not interested in the potential buffer overflow that may
446 result from a call to this function. Note the usage of the function
447 `nondet_int`: This is an internal SATABS-function that
448 nondeterministically returns an arbitrary integer value. The
449 function `__CPROVER_assume` tells SATABS to ignore all traces that
450 do not adhere to the given assumption. Therefore, whenever the lock
451 is held, `dummy_read` will return a value between 0 and `max`. If
452 the lock is not held, then `dummy_read` returns -1.
454 5. `dummy_release`: (in assets/driver.c) If the lock is held, then
455 `dummy_release` decreases the `usecount`, releases the lock, and
456 returns 0. Otherwise, the function returns -1.
458 We now want to check if any *valid* sequence of calls of the dispatch
459 functions (in driver.c) can lead to the violation of the assertion (in
460 assets/spec.c). Obviously, a call to `dummy_open` that is immediately
461 followed by a call to `unregister_chrdev` violates the assertion.
463 The function `main` in spec.c gives an example of how these functions
464 are called. First, a character device "`dummy`" is registered. The major
465 number is stored in the `inode` structure of the device. The values for
466 the file structure are assigned non-deterministically. We rule out
467 invalid sequences of calls by ensuring that no device is unregistered
468 while it is still locked. We use the following model checking harness
469 for calling the dispatching functions:
472 random = nondet_uchar ();
473 __CPROVER_assume (0 <= random && random <= 3);
478 rval = dummy_open (&inode, &my_file);
483 __CPROVER_assume (lock_held);
484 count = dummy_read (&my_file, buffer, BUF_SIZE);
487 dummy_release (&inode, &my_file);
495 The variable `random` is assigned non-deterministically. Subsequently,
496 the value of `random` is restricted to be 0 ≤ `random` ≤ 3 by a call
497 to `__CPROVER_assume`. Whenever the value of `random` is not in this
498 interval, the corresponding execution trace is simply discarded by
499 SATABS. Depending on the value of `random`, the harness calls either
500 `dummy_open`, `dummy_read` or `dummy_close`. Therefore, if there is a
501 sequence of calls to these three functions that leads to a violation of
502 the assertion in `unregister_chrdev`, then SATABS will eventually
505 If we ask SATABS to show us the properties it verifies with
507 satabs driver.c spec.c --show-properties
509 for our example, we obtain
511 1. Claim unregister\_chrdev.1:\
512 file spec.c line 18 function unregister\_chrdev\
513 MOD\_IN\_USE in unregister\_chrdev\
516 2. Claim dummy\_open.1:\
517 file driver.c line 15 function dummy\_open\
519 (unsigned int)inode->i\_rdev >> 8 == (unsigned
522 It seems obvious that the property dummy\_open.1 can never be violated.
523 SATABS confirms this assumption: We call
525 satabs driver.c spec.c --property dummy_open.1
527 and SATABS reports `VERIFICATION SUCCESSFUL` after a few iterations.
529 If we try to verify property unregister\_chrdev.1, SATABS reports that
530 the property in line 18 in file spec.c is violated (i.e., the assertion
531 does not hold, therefore the `VERIFICATION FAILED`). Furthermore, SATABS
532 provides a detailed description of the problem in the form of a
533 counterexample (i.e., an execution trace that violates the property). On
534 this trace, `dummy_open` is called **twice**, leading to a `usecount` of 2.
535 The second call of course fails with `rval=-1`, but the counter is
536 increased nevertheless:
539 int dummy_open (struct inode *inode, struct file *filp)
541 __CPROVER_assert(MAJOR (inode->i_rdev) == dummy_major,
549 return 0; /* success */
553 Then, `dummy_release` is called to release the lock on the device.
554 Finally, the loop is left and the call to `unregister_chrdev` results in
555 a violation of the assertion (since `usecount` is still 1, even though
558 \subsubsection man_satabs-tutorial-aeon Buffer Overflow in a Mail Transfer Agent
560 We explain how to model check Aeon version 0.2a, a small mail transfer
561 agent written by Piotr Benetkiewicz. The description advertises Aeon as
562 a "*good choice for **hardened** or minimalistic boxes*". The sources
564 [here](http://www.cprover.org/satabs/examples/loop_detection/aeon-0.2a.tar.gz).
566 Our first naive attempt to verify Aeon using
570 produces a positive result, but also warns us that the property holds
571 trivially. It also reveals that a large number library functions are
572 missing: SATABS is unable to find the source code for library functions
573 like `send`, `write` and `close`.
575 Now, do you have to provide a body for all missing library functions?
576 There is no easy answer to this question, but a viable answer would be
577 "most likely not". It is necessary to understand how SATABS handles
578 functions without bodies: It simply assumes that such a function returns
579 an arbitrary value, but that no other locations than the one on the left
580 hand side of the assignment are changed. Obviously, there are cases in
581 which this assumption is unsound, since the function potentially
582 modifies all memory locations that it can somehow address.
584 We now use static analysis to generate array bounds checks for Aeon:
586 satabs *.c --pointer-check --bounds-check --show-properties
588 SATABS will show about 300 properties in various functions (read
589 \ref man_instrumentation-properties "this" for more information on the
590 property instrumentation). Now consider the first few lines of the
591 `main` function of Aeon:
593 int main(int argc, char **argv)
595 char settings[MAX_SETTINGS][MAX_LEN];
597 numSet = getConfig(settings);
599 logEntry("Missing config file!");
604 and the function `getConfig` in `lib_aeon.c`:
606 int getConfig(char settings[MAX_SETTINGS][MAX_LEN])
609 FILE *fp; /* .rc file handler */
610 int numSet = 0; /* number of settings */
612 strcpy(home, getenv("HOME")); /* get home path */
613 strcat(home, "/.aeonrc"); /* full path to rc file */
614 fp = fopen(home, "r");
615 if (fp == NULL) return -1; /* no cfg - ERROR */
616 while (fgets(settings[numSet], MAX_LEN-1, fp)
617 && (numSet < MAX_SETTINGS)) numSet++;
623 The function `getConfig` makes calls to `strcpy`, `strcat`, `getenv`,
624 `fopen`, `fgets`, and `fclose`. It is very easy to provide an
625 implementation for the functions from the string library (string.h), and
626 SATABS comes with meaningful definitions for most of them. The
627 definition of `getenv` is not so straight-forward. The man-page of
628 `getenv` (which we obtain by entering `man 3 getenv` in a Unix or cygwin
629 command prompt) tells us:
631 `` `getenv' `` searches the list of environment variable names
632 and values (using the global pointer `char **environ`) for a
633 variable whose name matches the string at `NAME`. If a variable name
634 matches, `getenv` returns a pointer to the associated value.
636 SATABS has no information whatsoever about the content of `environ`.
637 Even if SATABS could access the environment variables on your
638 computer, a successful verification of `Aeon` would then only guarantee
639 that the properties for this program hold on your computer with a
640 specific set of environment variables. We have to assume that
641 `environ` contains environment variables that have an arbitrary
642 content of arbitrary length. The content of environment variables is
643 not only arbitrary but could be malefic, since it can be modified by the
644 user. The approximation of the behavior of `getenv` that is shipped with
645 SATABS completely ignores the content of the string.
647 Now let us have another look at the properties that SATABS generates for
648 the models of the string library and for `getenv`. Most of these
649 properties require that we verify that the upper and lower bounds of
650 buffers or arrays are not violated. Let us look at one of the properties
651 that SATABS generates for the code in function `getConfig`:
653 Claim getConfig.3: file lib_aeon.c line 19 function getConfig dereference failure: NULL plus offset pointer !(SAME-OBJECT(src, NULL))`
655 The model of the function `strcpy` dereferences the pointer returned by
656 `getenv`, which may return a NULL pointer. This possibility is detected
657 by the static analysis, and thus a corresponding property is generated.
658 Let us check this specific property:
660 satabs *.c --pointer-check --bounds-check --property getConfig.3
662 SATABS immediately returns a counterexample path that demonstrates how
663 `getenv` returns a NULL, which is subsequently dereferenced. We have
664 identified the first bug in this program: it requires that the
665 environment variable HOME is set, and crashes otherwise.
667 Let us examine one more property in the same function:
669 Claim getConfig.7: file lib_aeon.c line 19 function getConfig dereference failure: array `home' upper bound !(POINTER_OFFSET(dst) + (int)i >= 512) || !(SAME-OBJECT(dst, &home[0]))
671 This property asserts that the upper bound of the array `home` is not
672 violated. The variable `home` looks familiar: We encountered it in the
673 function `getConfig` given above. The function `getenv` in combination
674 with functions `strcpy`, `strcat` or `sprintf` is indeed often the
675 source for buffer overflows. Therefore, we try to use SATABS to check
676 the upper bound of the array `home`:
678 satabs *.c --pointer-check --bounds-check --property getConfig.7
680 SATABS runs for quite a while and will eventually give up, telling us
681 that its upper bound for abstraction refinement iterations has been
682 exceeded. This is not exactly the result we were hoping for, and we
683 could now increase the bound for iterations with help of the
684 `--iterations` command line switch of SATABS.
686 Before we do this, let us investigate why SATABS has failed to provide a
687 useful result. The function `strcpy` contains a loop that counts from 1
688 to the length of the input string. Predicate abstraction, the mechanism
689 SATABS is based on, is unable to detect such loops and will therefore
690 unroll the loop body as often as necessary. The array `home` has
691 `MAX_LEN` elements, and `MAX_LEN` is defined to be 512 in `aeon.h`.
692 Therefore, SATABS would have to run through at least 512 iterations,
693 only to verify (or reject) one of the more than 300 properties! Does
694 this fact defeat the purpose of static verification?
696 We can make the job easier: after reducing the value of `MAX_LEN` in
697 `aeon.h` to a small value, say to 10, SATABS provides a counterexample
698 trace that demonstrates how the buffer overflow be reproduced. If you
699 use the Eclipse plugin (as described \ref man_install-eclipse "here"),
700 you can step through this counterexample. The trace contains the string
701 that is returned by `getenv`.