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 [hardware/software co-verification](http://www.cprover.org/cprover-manual/hwsw.html).
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 [CBMC](http://www.cprover.org/cprover-manual/installation-cbmc.html)
136 and [SATABS](http://www.cprover.org/cprover-manual/installation-satabs.html).
138 Important note for Windows users: Visual Studio's `cl.exe` relies on a
139 complex set of environment variables to identify the target architecture
140 and the directories that contain the header files. You must run Eclipse
141 from within the *Visual Studio Command Prompt*.
143 \section man_satabs SATABS---Predicate Abstraction with SAT
145 \subsection man_satabs-overview Overview
147 This section describes SATABS from the point of view of the user. To
148 learn about the technology implemented in SATABS, read
149 \ref man_satabs-background "this".
151 We assume you have already installed SATABS and the necessary support
152 files on your system. If not so, please follow
153 \ref man_install-satabs "these instructions".
155 While users of SATABS almost never have to be concerned about the
156 underlying refinement abstraction algorithms, understanding the classes
157 of properties that can be verified is crucial. Predicate abstraction is
158 most effective when applied to *control-flow dominated properties*. As
159 an example, reconsider the following program (lock-example-fixed.c):
180 unsigned got_lock = 0;
186 /* critical section */
199 The two assertions in the program model that the functions `lock()` and
200 `unlock()` are called in the right order. Note that the value of `times`
201 is chosen non-deterministically and is not bounded. The program has no
202 run-time bound, and thus, unwinding the code with CBMC will never
205 ### Working with Claims
207 The two assertions will give rise to two *properties*. Each property is
208 associated to a specific line of code, i.e., a property is violated when
209 some condition can become false at the corresponding program location.
210 SATABS will generate a list of all properties for the programs as
213 satabs lock-example-fixed.c --show-properties
215 SATABS will list two properties; each property corresponds to one of the
216 two assertions. We can use SATABS to verify both properties as follows:
218 satabs lock-example-fixed.c
220 SATABS will conclude the verification successfully, that is, both
221 assertions hold for execution traces of any length.
223 By default, SATABS attempts to verify all properties at once. A single
224 property can be verified (or refuted) by using the `--property id`
225 option of SATABS, where `id` denotes the identifier of the property in
226 the list obtained by calling SATABS with the `--show-properties` flag.
227 Whenever a property is violated, SATABS reports a feasible path that
228 leads to a state in which the condition that corresponds to the violated
229 property evaluates to false.
231 \subsection man_satabs-libraries Programs that use Libraries
233 SATABS cannot check programs that use functions that are only available
234 in binary (compiled) form (this restriction is not imposed by the
235 verification algorithms that are used by SATABS – they also work on
236 assembly code). The reason is simply that so far no assembly language
237 frontend is available for SATABS. At the moment, (library) functions for
238 which no C source code is available have to be replaced by stubs. The
239 usage of stubs and harnesses (as known from unit testing) also allows to
240 check more complicated properties (like, for example, whether function
241 `fopen` is always called before `fclose`). This technique is explained
242 in detail in the \ref man_satabs-tutorials "SATABS tutorials".
244 \subsection man_satabs-unit-test Unit Testing with SATABS
246 The example presented \ref man_satabs-tutorial-driver "here" is
247 obviously a toy example and can hardly be used to convince your project
248 manager to use static verification in your next project. Even though we
249 recommend to use formal verification and specification already in the
250 early phases of your project, the sad truth is that in most projects
251 verification (of any kind) is still pushed to the very end of the
252 development cycle. Therefore, this section is dedicated to the
253 verification of legacy code. However, the techniques presented here can
254 also be used for *unit testing*.
256 Unit testing is used in most software development projects, and static
257 verification with SATABS can be very well combined with this technique.
258 Unit testing relies on a number test cases that yield the desired code
259 coverage. Such test cases are implemented by a software testing engineer
260 in terms of a test harness (aka test driver) and a set of function
261 stubs. Typically, a slight modification to the test harness allows it to
262 be used with SATABS. Replacing the explicit input values with
263 non-deterministic inputs (as explained in
264 \ref man_satabs-tutorial-aeon "here" and
265 \ref man_satabs-tutorial-driver "here")) guarantees that SATABS will try
266 to achieve **full** path and state coverage (due to the fact that
267 predicate abstraction implicitly detects equivalence classes). However,
268 it is not guaranteed that SATABS terminates in all cases. Keep in mind
269 that you must not make any assumptions about the validity of the
270 properties if SATABS did not run to completion!
274 - [Model Checking Concurrent Linux Device
275 Drivers](http://www.kroening.com/publications/view-publications-wbwk2007.html)
276 - [SATABS: SAT-based Predicate Abstraction for
277 ANSI-C](http://www-2.cs.cmu.edu/~svc/papers/view-publications-cksy2005.html)
278 - [Predicate Abstraction of ANSI-C Programs using
279 SAT](http://www-2.cs.cmu.edu/~svc/papers/view-publications-cksy2004.html)
281 \subsection man_satabs-background Background
283 ### Sound Abstractions
285 This section provides background information on how SATABS operates.
286 Even for very trivial C programs it is impossible to exhaustively
287 examine their state space (which is potentially unbounded). However, not
288 all details in a C program necessarily contribute to a bug, so it may be
289 sufficient to only examine those parts of the program that are somehow
292 In practice, many static verification tools (such as `lint`) try to
293 achieve this goal by applying heuristics. This approach comes at a cost:
294 bugs might be overlooked because the heuristics do not cover all
295 relevant aspects of the program. Therefore, the conclusion that a
296 program is correct whenever such a static verification tool is unable to
297 find an error is invalid.
299 \image html cegar-1.png "CEGAR Loop"
301 A more sophisticated approach that has been very successful recently is
302 to generate a *sound* abstraction of the original program. In this
303 context, *soundness* refers to the fact that the abstract program
304 contains (at least) all relevant behaviors (i.e., bugs) that are present
305 in the original program. In the Figure above, the first component strips
306 details from the original program. The number of possible behaviors
307 increases as the number of details in the abstract program decreases.
308 Intuitively, the reason is that whenever the model checking tool lacks
309 the information that is necessary to make an accurate decision on
310 whether a branch of an control flow statement can be taken or not, both
311 branches have to be considered.
313 In the resulting *abstract program*, a set of concrete states is
314 subsumed by means of a single abstract state. Consider the following
319 The concrete states *x*~1~ and *x*~2~ are mapped to an abstract state
320 *X*, and similarly *Y* subsumes *y*~1~ and *y*~2~. However, all
321 transitions that are possible in the concrete program are also possible
322 in the abstract model. The abstract transition *X* → *Y* summarizes the
323 concrete transitions *x*~1~ → *y*~1~ and *x*~1~ → *x*~1~, and *Y* → *X*
324 corresponds to *x*~1~ → *x*~2~. The behavior *X* → *Y* → *X* is feasible
325 in the original program, because it maps to *x*~1~ → *x*~1~ → *x*~2~.
326 However, *Y* → *X* → *Y* is feasible only in the abstract model.
328 ### Spurious Counterexamples
330 The consequence is that the model checker (component number two in the
331 figure above) possibly reports a *spurious* counterexample. We call a
332 counterexample spurious whenever it is feasible in the current abstract
333 model but not in the original program. However, whenever the model
334 checker is unable to find an execution trace that violates the given
335 property, we can conclude that there is no such trace in the original
338 The feasibility of counterexamples is checked by *symbolic simulation*
339 (performed by component three in the figure above). If the
340 counterexample is indeed feasible, SATABS found a bug in the original
341 program and reports it to the user.
343 ### Automatic Refinement
345 On the other hand, infeasible counterexamples (that originate from
346 abstract behaviors that result from the omission of details and are not
347 present in the original program) are never reported to the user.
348 Instead, the information is used in order to refine the abstraction such
349 that the spurious counterexample is not part of the refined model
350 anymore. For instance, the reason for the infeasibility of *Y* → *X* →
351 *Y* is that neither *y*~1~ nor *x*~1~ can be reached from *x*~2~.
352 Therefore, the abstraction can be refined by partitioning *X*.
354 The refinement steps can be illustrated as follows:
356 
358 The first step (1) is to generate a very coarse abstraction with a very
359 small state space. This abstraction is then successively refined (2, 3,
360 ...) until either a feasible counterexample is found or the abstract
361 program is detailed enough to show that there is no path that leads to a
362 violation of the given property. The problem is that this point is not
363 necessarily reached for every input program, i.e., it is possible that
364 the the abstraction refinement loop never terminates. Therefore, SATABS
365 allows to specify an upper bound for the number of iterations.
367 When this upper bound is reached and no counterexample was found, this
368 does not necessarily mean that there is none. In this case, you cannot
369 make any conclusions at all with respect to the correctness of the input
372 \subsection man_satabs-tutorials Tutorials
374 We provide an introduction to model checking "real" C programs with
375 SATABS using two small examples.
377 \subsubsection man_satabs-tutorial-driver Reference Counting in Linux Device Drivers
379 Microsoft's [SLAM](http://research.microsoft.com/SLAM) toolkit has been
380 successfully used to find bugs in Windows device drivers. SLAM
381 automatically verifies device driver whether a device driver adheres to
382 a set of specifications. SLAM provides a test harness for device drivers
383 that calls the device driver dispatch routines in a non-deterministic
384 order. Therefore, the Model Checker examines all combinations of calls.
385 Motivated by the success this approach, we provide a toy example based
386 on Linux device drivers. For a more complete approach to the
387 verification of Linux device drivers, consider
388 [DDVerify](http://www.cprover.org/ddverify/).
390 Dynamically loadable modules enable the Linux Kernel to load device
391 drivers on demand and to release them when they are not needed anymore.
392 When a device driver is registered, the kernel provides a major number
393 that is used to uniquely identify the device driver. The corresponding
394 device can be accessed through special files in the filesystem; by
395 convention, they are located in the `/dev` directory. If a process
396 accesses a device file the kernel calls the corresponding `open`, `read`
397 and `write` functions of the device driver. Since a driver must not be
398 released by the kernel as long as it is used by at least one process,
399 the device driver must maintain a usage counter (in more recent Linux
400 kernels, this is done automatically, however, drivers that must maintain
401 backward compatibility have to adjust this counter).
403 We provide a skeleton of such a driver. Download the files
404 assets/spec.c, assets/driver.c, assets/driver.h, assets/kdev_t.h, and
407 The driver contains following functions:
409 1. `register_chrdev`: (in assets/spec.c) Registers a character device.
410 In our implementation, the function sets the variable `usecount` to
411 zero and returns a major number for this device (a constant, if the
412 user provides 0 as argument for the major number, and the value
413 specified by the user otherwise).
417 int register_chrdev (unsigned int major, const char* name)
425 2. `unregister_chrdev`: (in assets/spec.c) Unregisters a character
426 device. This function asserts that the device is not used by any
427 process anymore (we use the macro `MOD_IN_USE` to check this).
429 int unregister_chrdev (unsigned int major, const char* name)
439 3. `dummy_open`: (in assets/driver.c) This function increases the
440 `usecount`. If the device is locked by some other process
441 `dummy_open` returns -1. Otherwise it locks the device for the
444 4. `dummy_read`: (in assets/driver.c) This function "simulates" a read
445 access to the device. In fact it does nothing, since we are
446 currently not interested in the potential buffer overflow that may
447 result from a call to this function. Note the usage of the function
448 `nondet_int`: This is an internal SATABS-function that
449 nondeterministically returns an arbitrary integer value. The
450 function `__CPROVER_assume` tells SATABS to ignore all traces that
451 do not adhere to the given assumption. Therefore, whenever the lock
452 is held, `dummy_read` will return a value between 0 and `max`. If
453 the lock is not held, then `dummy_read` returns -1.
455 5. `dummy_release`: (in assets/driver.c) If the lock is held, then
456 `dummy_release` decreases the `usecount`, releases the lock, and
457 returns 0. Otherwise, the function returns -1.
459 We now want to check if any *valid* sequence of calls of the dispatch
460 functions (in driver.c) can lead to the violation of the assertion (in
461 assets/spec.c). Obviously, a call to `dummy_open` that is immediately
462 followed by a call to `unregister_chrdev` violates the assertion.
464 The function `main` in spec.c gives an example of how these functions
465 are called. First, a character device "`dummy`" is registered. The major
466 number is stored in the `inode` structure of the device. The values for
467 the file structure are assigned non-deterministically. We rule out
468 invalid sequences of calls by ensuring that no device is unregistered
469 while it is still locked. We use the following model checking harness
470 for calling the dispatching functions:
473 random = nondet_uchar ();
474 __CPROVER_assume (0 <= random && random <= 3);
479 rval = dummy_open (&inode, &my_file);
484 __CPROVER_assume (lock_held);
485 count = dummy_read (&my_file, buffer, BUF_SIZE);
488 dummy_release (&inode, &my_file);
496 The variable `random` is assigned non-deterministically. Subsequently,
497 the value of `random` is restricted to be 0 ≤ `random` ≤ 3 by a call
498 to `__CPROVER_assume`. Whenever the value of `random` is not in this
499 interval, the corresponding execution trace is simply discarded by
500 SATABS. Depending on the value of `random`, the harness calls either
501 `dummy_open`, `dummy_read` or `dummy_close`. Therefore, if there is a
502 sequence of calls to these three functions that leads to a violation of
503 the assertion in `unregister_chrdev`, then SATABS will eventually
506 If we ask SATABS to show us the properties it verifies with
508 satabs driver.c spec.c --show-properties
510 for our example, we obtain
512 1. Claim unregister\_chrdev.1:\
513 file spec.c line 18 function unregister\_chrdev\
514 MOD\_IN\_USE in unregister\_chrdev\
517 2. Claim dummy\_open.1:\
518 file driver.c line 15 function dummy\_open\
520 (unsigned int)inode->i\_rdev >> 8 == (unsigned
523 It seems obvious that the property dummy\_open.1 can never be violated.
524 SATABS confirms this assumption: We call
526 satabs driver.c spec.c --property dummy_open.1
528 and SATABS reports `VERIFICATION SUCCESSFUL` after a few iterations.
530 If we try to verify property unregister\_chrdev.1, SATABS reports that
531 the property in line 18 in file spec.c is violated (i.e., the assertion
532 does not hold, therefore the `VERIFICATION FAILED`). Furthermore, SATABS
533 provides a detailed description of the problem in the form of a
534 counterexample (i.e., an execution trace that violates the property). On
535 this trace, `dummy_open` is called **twice**, leading to a `usecount` of 2.
536 The second call of course fails with `rval=-1`, but the counter is
537 increased nevertheless:
540 int dummy_open (struct inode *inode, struct file *filp)
542 __CPROVER_assert(MAJOR (inode->i_rdev) == dummy_major,
550 return 0; /* success */
554 Then, `dummy_release` is called to release the lock on the device.
555 Finally, the loop is left and the call to `unregister_chrdev` results in
556 a violation of the assertion (since `usecount` is still 1, even though
559 \subsubsection man_satabs-tutorial-aeon Buffer Overflow in a Mail Transfer Agent
561 We explain how to model check Aeon version 0.2a, a small mail transfer
562 agent written by Piotr Benetkiewicz. The description advertises Aeon as
563 a "*good choice for **hardened** or minimalistic boxes*". The sources
565 [here](http://www.cprover.org/satabs/examples/loop_detection/aeon-0.2a.tar.gz).
567 Our first naive attempt to verify Aeon using
571 produces a positive result, but also warns us that the property holds
572 trivially. It also reveals that a large number library functions are
573 missing: SATABS is unable to find the source code for library functions
574 like `send`, `write` and `close`.
576 Now, do you have to provide a body for all missing library functions?
577 There is no easy answer to this question, but a viable answer would be
578 "most likely not". It is necessary to understand how SATABS handles
579 functions without bodies: It simply assumes that such a function returns
580 an arbitrary value, but that no other locations than the one on the left
581 hand side of the assignment are changed. Obviously, there are cases in
582 which this assumption is unsound, since the function potentially
583 modifies all memory locations that it can somehow address.
585 We now use static analysis to generate array bounds checks for Aeon:
587 satabs *.c --pointer-check --bounds-check --show-properties
589 SATABS will show about 300 properties in various functions (read
590 [this](http://www.cprover.org/cprover-manual/properties.html) for
591 more information on the property instrumentation).
592 Now consider the first few lines of the `main` function of Aeon:
594 int main(int argc, char **argv)
596 char settings[MAX_SETTINGS][MAX_LEN];
598 numSet = getConfig(settings);
600 logEntry("Missing config file!");
605 and the function `getConfig` in `lib_aeon.c`:
607 int getConfig(char settings[MAX_SETTINGS][MAX_LEN])
610 FILE *fp; /* .rc file handler */
611 int numSet = 0; /* number of settings */
613 strcpy(home, getenv("HOME")); /* get home path */
614 strcat(home, "/.aeonrc"); /* full path to rc file */
615 fp = fopen(home, "r");
616 if (fp == NULL) return -1; /* no cfg - ERROR */
617 while (fgets(settings[numSet], MAX_LEN-1, fp)
618 && (numSet < MAX_SETTINGS)) numSet++;
624 The function `getConfig` makes calls to `strcpy`, `strcat`, `getenv`,
625 `fopen`, `fgets`, and `fclose`. It is very easy to provide an
626 implementation for the functions from the string library (string.h), and
627 SATABS comes with meaningful definitions for most of them. The
628 definition of `getenv` is not so straight-forward. The man-page of
629 `getenv` (which we obtain by entering `man 3 getenv` in a Unix or cygwin
630 command prompt) tells us:
632 `` `getenv' `` searches the list of environment variable names
633 and values (using the global pointer `char **environ`) for a
634 variable whose name matches the string at `NAME`. If a variable name
635 matches, `getenv` returns a pointer to the associated value.
637 SATABS has no information whatsoever about the content of `environ`.
638 Even if SATABS could access the environment variables on your
639 computer, a successful verification of `Aeon` would then only guarantee
640 that the properties for this program hold on your computer with a
641 specific set of environment variables. We have to assume that
642 `environ` contains environment variables that have an arbitrary
643 content of arbitrary length. The content of environment variables is
644 not only arbitrary but could be malefic, since it can be modified by the
645 user. The approximation of the behavior of `getenv` that is shipped with
646 SATABS completely ignores the content of the string.
648 Now let us have another look at the properties that SATABS generates for
649 the models of the string library and for `getenv`. Most of these
650 properties require that we verify that the upper and lower bounds of
651 buffers or arrays are not violated. Let us look at one of the properties
652 that SATABS generates for the code in function `getConfig`:
654 Claim getConfig.3: file lib_aeon.c line 19 function getConfig dereference failure: NULL plus offset pointer !(SAME-OBJECT(src, NULL))`
656 The model of the function `strcpy` dereferences the pointer returned by
657 `getenv`, which may return a NULL pointer. This possibility is detected
658 by the static analysis, and thus a corresponding property is generated.
659 Let us check this specific property:
661 satabs *.c --pointer-check --bounds-check --property getConfig.3
663 SATABS immediately returns a counterexample path that demonstrates how
664 `getenv` returns a NULL, which is subsequently dereferenced. We have
665 identified the first bug in this program: it requires that the
666 environment variable HOME is set, and crashes otherwise.
668 Let us examine one more property in the same function:
670 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]))
672 This property asserts that the upper bound of the array `home` is not
673 violated. The variable `home` looks familiar: We encountered it in the
674 function `getConfig` given above. The function `getenv` in combination
675 with functions `strcpy`, `strcat` or `sprintf` is indeed often the
676 source for buffer overflows. Therefore, we try to use SATABS to check
677 the upper bound of the array `home`:
679 satabs *.c --pointer-check --bounds-check --property getConfig.7
681 SATABS runs for quite a while and will eventually give up, telling us
682 that its upper bound for abstraction refinement iterations has been
683 exceeded. This is not exactly the result we were hoping for, and we
684 could now increase the bound for iterations with help of the
685 `--iterations` command line switch of SATABS.
687 Before we do this, let us investigate why SATABS has failed to provide a
688 useful result. The function `strcpy` contains a loop that counts from 1
689 to the length of the input string. Predicate abstraction, the mechanism
690 SATABS is based on, is unable to detect such loops and will therefore
691 unroll the loop body as often as necessary. The array `home` has
692 `MAX_LEN` elements, and `MAX_LEN` is defined to be 512 in `aeon.h`.
693 Therefore, SATABS would have to run through at least 512 iterations,
694 only to verify (or reject) one of the more than 300 properties! Does
695 this fact defeat the purpose of static verification?
697 We can make the job easier: after reducing the value of `MAX_LEN` in
698 `aeon.h` to a small value, say to 10, SATABS provides a counterexample
699 trace that demonstrates how the buffer overflow be reproduced. If you
700 use the Eclipse plugin (as described
701 [here](http://www.cprover.org/cprover-manual/installation-plugin.html)),
702 you can step through this counterexample. The trace contains the string
703 that is returned by `getenv`.