cprover
/builddir/build/BUILD/cbmc-cbmc-5.10/doc/satabs-user-manual.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page other_documentation Other Documentation
3 
4 \section satabs SATABS
5 
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.
10 
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
18 for
19 \ref man_hard-soft-introduction "hardware/software co-verification".
20 
21 ## Automatic Program Verification with SATABS
22 
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.
27 
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".
32 We also provide
33 \ref man_satabs-tutorials "tutorials on how to use SATABS".
34 
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.
38 
39 \subsection man_install-satabs Installing SATABS
40 
41 ### Requirements
42 
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.
46 
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
52  Studio
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.
56 
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*.
61 
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.
67 
68 ### Choosing and Installing a Model Checker
69 
70 You need to install a Model Checker in order to be able to run SATABS.
71 You can choose between following alternatives:
72 
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.
84 
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
90 
91  --modelchecker nusmv
92 
93  to instruct SATABS to use NuSMV.
94 
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
102 
103  --modelchecker boppo
104 
105  when you call SATABS and want it to use BOPPO instead of SMV.
106 
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.
110 
111 ### Installing SATABS
112 
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.
117 
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.
122 
123 ### Requirements
124 
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.
131 
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".
136 
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*.
141 
142 \section man_satabs SATABS---Predicate Abstraction with SAT
143 
144 \subsection man_satabs-overview Overview
145 
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".
149 
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".
153 
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):
159 
160 ```
161  _Bool nondet_bool();
162  _Bool LOCK = 0;
163 
164  _Bool lock() {
165  if(nondet_bool()) {
166  assert(!LOCK);
167  LOCK=1;
168  return 1; }
169 
170  return 0;
171  }
172 
173  void unlock() {
174  assert(LOCK);
175  LOCK=0;
176  }
177 
178  int main() {
179  unsigned got_lock = 0;
180  int times;
181 
182  while(times > 0) {
183  if(lock()) {
184  got_lock++;
185  /* critical section */
186  }
187 
188  if(got_lock!=0) {
189  unlock();
190  got_lock--;
191  }
192 
193  times--;
194  }
195  }
196 ```
197 
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
202 terminate.
203 
204 ### Working with Claims
205 
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
210 follows:
211 
212  satabs lock-example-fixed.c --show-properties
213 
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:
216 
217  satabs lock-example-fixed.c
218 
219 SATABS will conclude the verification successfully, that is, both
220 assertions hold for execution traces of any length.
221 
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.
229 
230 \subsection man_satabs-libraries Programs that use Libraries
231 
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".
242 
243 \subsection man_satabs-unit-test Unit Testing with SATABS
244 
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*.
254 
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!
270 
271 ### Further Reading
272 
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)
279 
280 \subsection man_satabs-background Background
281 
282 ### Sound Abstractions
283 
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
289 related to a bug.
290 
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.
297 
298 \image html cegar-1.png "CEGAR Loop"
299 
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.
311 
312 In the resulting *abstract program*, a set of concrete states is
313 subsumed by means of a single abstract state. Consider the following
314 figure:
315 
316 ![](states.png)
317 
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.
326 
327 ### Spurious Counterexamples
328 
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
335 program, either.
336 
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.
341 
342 ### Automatic Refinement
343 
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*.
352 
353 The refinement steps can be illustrated as follows:
354 
355 ![Iterative refinement](refinement.png)
356 
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.
365 
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
369 program.
370 
371 \subsection man_satabs-tutorials Tutorials
372 
373 We provide an introduction to model checking "real" C programs with
374 SATABS using two small examples.
375 
376 \subsubsection man_satabs-tutorial-driver Reference Counting in Linux Device Drivers
377 
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/).
388 
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).
401 
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
404 assets/modules.h.
405 
406 The driver contains following functions:
407 
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).
413 
414  int usecount;
415 
416  int register_chrdev (unsigned int major, const char* name)
417  {
418  usecount = 0;
419  if (major == 0)
420  return MAJOR_NUMBER;
421  return major;
422  }
423 
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).
427 
428  int unregister_chrdev (unsigned int major, const char* name)
429  {
430  if (MOD_IN_USE)
431  {
432  ERROR: assert (0);
433  }
434  else
435  return 0;
436  }
437 
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
441  caller.
442 
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  non­determi­nistically 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.
453 
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.
457 
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.
462 
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:
470 
471 ```
472  random = nondet_uchar ();
473  __CPROVER_assume (0 <= random && random <= 3);
474 
475  switch (random)
476  {
477  case 1:
478  rval = dummy_open (&inode, &my_file);
479  if (rval == 0)
480  lock_held = TRUE;
481  break;
482  case 2:
483  __CPROVER_assume (lock_held);
484  count = dummy_read (&my_file, buffer, BUF_SIZE);
485  break;
486  case 3:
487  dummy_release (&inode, &my_file);
488  lock_held = FALSE;
489  break;
490  default:
491  break;
492  }
493 ```
494 
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
503 consider it.
504 
505 If we ask SATABS to show us the properties it verifies with
506 
507  satabs driver.c spec.c --show-properties
508 
509 for our example, we obtain
510 
511 1. Claim unregister\_chrdev.1:\
512      file spec.c line 18 function unregister\_chrdev\
513      MOD\_IN\_USE in unregister\_chrdev\
514      FALSE
515 
516 2. Claim dummy\_open.1:\
517      file driver.c line 15 function dummy\_open\
518      i\_rdev mismatch\
519      (unsigned int)inode-&gt;i\_rdev &gt;&gt; 8 == (unsigned
520  int)dummy\_major
521 
522 It seems obvious that the property dummy\_open.1 can never be violated.
523 SATABS confirms this assumption: We call
524 
525  satabs driver.c spec.c --property dummy_open.1
526 
527 and SATABS reports `VERIFICATION SUCCESSFUL` after a few iterations.
528 
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:
537 
538 ```
539  int dummy_open (struct inode *inode, struct file *filp)
540  {
541  __CPROVER_assert(MAJOR (inode->i_rdev) == dummy_major,
542  "i_rdev mismatch");
543  MOD_INC_USE_COUNT;
544 
545  if (locked)
546  return -1;
547  locked = TRUE;
548 
549  return 0; /* success */
550  }
551  ```
552 
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
556 `locked=0`).
557 
558 \subsubsection man_satabs-tutorial-aeon Buffer Overflow in a Mail Transfer Agent
559 
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
563 are available
564 [here](http://www.cprover.org/satabs/examples/loop_detection/aeon-0.2a.tar.gz).
565 
566 Our first naive attempt to verify Aeon using
567 
568  satabs *.c
569 
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`.
574 
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 un­sound, since the function potentially
582 modifies all memory locations that it can somehow address.
583 
584 We now use static analysis to generate array bounds checks for Aeon:
585 
586  satabs *.c --pointer-check --bounds-check --show-properties
587 
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:
592 
593  int main(int argc, char **argv)
594  {
595  char settings[MAX_SETTINGS][MAX_LEN];
596  ...
597  numSet = getConfig(settings);
598  if (numSet == -1) {
599  logEntry("Missing config file!");
600  exit(1);
601  }
602  ...
603 
604 and the function `getConfig` in `lib_aeon.c`:
605 
606  int getConfig(char settings[MAX_SETTINGS][MAX_LEN])
607  {
608  char home[MAX_LEN];
609  FILE *fp; /* .rc file handler */
610  int numSet = 0; /* number of settings */
611 
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++;
618  fclose(fp);
619 
620  return numSet;
621  }
622 
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:
630 
631  `` `getenv' `` searches the list of en­vi­ron­ment 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.
635 
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 en­vi­ron­ment variables. We have to assume that
641 `environ` contains en­vi­ron­ment variables that have an arbitrary
642 content of arbitrary length. The content of en­vi­ron­ment 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.
646 
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`:
652 
653  Claim getConfig.3:   file lib_aeon.c line 19 function getConfig   dereference failure: NULL plus offset pointer   !(SAME-OBJECT(src, NULL))`
654 
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:
659 
660  satabs *.c --pointer-check --bounds-check --property getConfig.3
661 
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.
666 
667 Let us examine one more property in the same function:
668 
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]))
670 
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`:
677 
678  satabs *.c --pointer-check --bounds-check --property getConfig.7
679 
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.
685 
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?
695 
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`.