Added more documentation to checks (#26)

* Added more documentation to checks

* Corrected typo in opam files

* Added documentation command to makefile

* updated documentation build command in Readme.md

* Fixed some documentation typos

* rand without srand is always treated as an anti-pattern.

* delete generated documentation on "make clean"

.gitignore

@@ -219,6 +219,9 @@ test/run_real_world_samples.sh
 # install files for opam packages (generated by dune)
 *.install
 
+# the documentation build directory
+doc/html
+
 test/artificial_samples/dockcross*
 
 .#*

CHANGES.md

+dev
+====
+
+-   Added more documentation to checks (PR #26)
+
 0.2 (2019-06-25)
 =====
 

Makefile

@@ -15,6 +15,7 @@ test:
 clean:
 	dune clean
 	bapbuild -clean
+	rm -f -r doc/html
 	cd test/unit; make clean; cd ../..
 	cd plugins/cwe_checker; make clean; cd ../..
 	cd plugins/cwe_checker_emulation; make clean; cd ../..
@@ -28,5 +29,9 @@ uninstall:
 	cd plugins/cwe_checker_type_inference; make uninstall; cd ../..
 	cd plugins/cwe_checker_type_inference_print; make uninstall; cd ../..
 
+documentation:
+	dune build @doc
+	cp -r _build/default/_doc/_html doc/html
+
 docker:
 	./install.sh

README.md

@@ -61,8 +61,9 @@ If you plan to develop cwe_checker, it is recommended to build it using the prov
 -   Sark (latest) for IDA Pro annotations
 -   pytest >= 3.5.1 (for tests)
 -   SCons >= 3.0.5 (for tests)
+-   odoc >= 1.4 (for documentation)
 
-Just run `make all` to compile and register the plugin with BAP. You can run the test suite via `make test`.
+Just run `make all` to compile and register the plugin with BAP. You can run the test suite via `make test`. Documentation can be built via `make documentation`.
 ## How to use cwe_checker? ##
 The usage is straight forward: adjust the `config.json` (if needed) and call BAP with *cwe_checker* as a pass.
 ``` bash
@@ -84,7 +85,7 @@ If you plan to open a PR, please utilize [precommit](https://pre-commit.com) in
 ### Contribute ###
 Contributions are always welcome. Just fork it and open a pull request!
 ## How does cwe_checker work internally? ##
-Naturally, the most accurate documentation is the source code. At the moment, we provide documentation in the *doc/*. This includes documentation of how to solve certain tasks with cwe_checker (e.g. implement your own plugin) and also the slides conference presentations on cwe_checker. The slides about cwe_checker should be of special interest for those who would like to get a quick/initial overview of its internals. 
+Documentation can be built via `make documentation` and the found in *doc/html/*. But the most accurate documentation is still the source code. We provide some more information in *doc/*, including the slides of conference presentations on cwe_checker. These should be of special interest for those who would like to get a quick/initial overview of its internals. 
 
 We presented cwe_checker at the following conferences so far:
 - [Pass The SALT 2019](https://2019.pass-the-salt.org/talks/74.html) ([slides](doc/slides/cwe_checker_pts19.pdf))

cwe_checker.opam

@@ -19,6 +19,7 @@ depends: [
   "alcotest" {>= "0.8.3"}
   "core_kernel" {>= "v0.11" & < "v0.12"}
   "ppx_jane" {>= "v0.11" & < "v0.12"}
+  "odoc" {>= "1.4"}
 ]
 depexts: [
   "binutils"

src/checkers/cwe_190.mli

-(** TODO
-CWE-190 (Integer Overflow or Wraparound)
-https://cwe.mitre.org/data/definitions/190.html
+(** This module implements a check for CWE-190: Integer overflow or wraparound.
+
+    An integer overflow can lead to undefined behaviour and is especially dangerous
+    in conjunction with memory management functions.
+
+    See {: https://cwe.mitre.org/data/definitions/190.html} for a detailed description.
+
+    {1 How the check works}
+
+    For each call to a function from the CWE190 symbol list we check whether the
+    basic block directly before the call contains a multiplication instruction.
+    If one is found, the call gets flagged as a CWE hit, as there is no overflow
+    check corresponding to the multiplication befor the call. The default CWE190
+    symbol list contains the memory allocation functions {i malloc}, {i xmalloc},
+    {i calloc} and {i realloc}. The list is configurable in config.json.
+
+    {1 False Positives}
+
+    - There is no check whether the result of the multiplication is actually used
+      as input to the function call. However, this does not seem to generate a lot
+      of false positives in practice.
+    - There is no value set analysis in place to determine whether an overflow is
+      possible or not at the specific instruction.
+
+    {1 False Negatives}
+
+    - All integer overflows not in a basic block right before a call to a function
+    from the CWE190 symbol list.
+    - All integer overflows caused by addition or subtraction.
 *)
+
 val name : string
 val version : string
 

src/checkers/cwe_215.mli

-(**  This module checks if a binary contains sensitive debugging information that could be leveraged to
-   get a better understanding of it in less time. This is basically CWE-215 (https://cwe.mitre.org/data/definitions/215.html *)
+(** This module implements a check for CWE-215: Information Exposure Through Debug Information.
+
+    Sensitive debugging information can be leveraged to get a better understanding
+    of a binary in less time.
+
+    See {: https://cwe.mitre.org/data/definitions/215.html} for a detailed description.
+
+    {1 How the check works}
+
+    The binary is checked for debug strings using readelf.
+
+    {1 False Positives}
+
+    None known.
+
+    {1 False Negatives}
+
+    - There may be other debug information not found by readelf.
+*)
+
 val name : string
 val version : string
 

src/checkers/cwe_243.mli

-(** This module implements a check for CWE-243 (Creation of chroot Jail Without Changing Working Directory).
-According to http://www.unixwiz.net/techtips/chroot-practices.html, there are several ways to achieve the
-safe creation of a chroot jail, e.g. chdir -> chroot -> setuid. They are configurable in config.json.
-See https://cwe.mitre.org/data/definitions/243.html for detailed description. *)
+(** This module implements a check for CWE-243: Creation of chroot Jail Without Changing Working Directory.
+
+    Creating a chroot Jail without changing the working directory afterwards does
+    not prevent access to files outside of the jail.
+
+    See {: https://cwe.mitre.org/data/definitions/243.html} for detailed a description.
+
+    {1 How the check works}
+
+    According to {: http://www.unixwiz.net/techtips/chroot-practices.html}, there are
+    several ways to achieve the safe creation of a chroot jail, e.g. chdir -> chroot -> setuid.
+    They are configurable in config.json. We check whether each function that calls
+    chroot is using one of these safe call sequences to do so. If not, a warning is emitted.
+
+    {1 False Positives}
+
+    None known.
+
+    {1 False Negatives}
+
+    None known.
+*)
+
 val name : string
 val version : string
 

src/checkers/cwe_248.mli

-(** This module implements a check for CWE-248 (Uncaught Exception)
-An uncaught exception may lead to a crash and subsequentially to other unintended behavior.
-See https://cwe.mitre.org/data/definitions/248.html for detailed description.
+(** This module implements a check for CWE-248: Uncaught Exception.
+
+    An uncaught exception may lead to a crash.
+
+    See {: https://cwe.mitre.org/data/definitions/248.html} for a detailed description.
+
+    {1 How the check works}
+
+    The tool searches for exception throws that are reachable in the callgraph without
+    touching a function that contains a catch block. We do not check whether a catch block
+    can actually catch the thrown exceptions, thus we generate some false negatives.
+
+    {1 False Positives}
+
+    - There is no check whether a specific exception throw can be triggered or not
+
+    {1 False Negatives}
+
+    - An exception that gets catched through one execution path but would not get
+    catched through a different execution path will not get flagged.
+    - It is not checked whether the catch block can actually catch a thrown exception
+    or not. A catch block may only be able to catch exceptions of a specific type.
+*)
 
-Right now we search for exception throws that are reachable in the callgraph without
-touching a function that contains a catch block. We do not check whether a catch block
-can actually catch the thrown exceptions, thus we generate some false negatives. **)
 val name : string
 val version : string
 

src/checkers/cwe_332.mli

-(** This module implements a check for CWE332 (Insufficient Entropy in PRNG).
-This can happen, for instance, if the PRNG is not seeded. A classical example
-would be calling rand without srand. This could lead to predictable random
-numbers and could, for example, weaken crypto functionality.
-See https://cwe.mitre.org/data/definitions/332.html for detailed description. *)
+(** This module implements a check for CWE332: Insufficient Entropy in PRNG.
+
+    This can happen, for instance, if the PRNG is not seeded. A classical example
+    would be calling rand without srand. This could lead to predictable random
+    numbers and could, for example, weaken crypto functionality.
+
+    See {: https://cwe.mitre.org/data/definitions/332.html} for a detailed description.
+
+    {1 How the check works}
+
+    We check whether the program calls rand but not srand.
+
+    {1 False Positives}
+
+    None known
+
+    {1 False Negatives}
+
+    - It is not checked whether srand gets called before rand
+*)
+
 val name : string
 val version : string
 

src/checkers/cwe_367.mli

-(** TODO
-CWE-367 (Time-of-check Time-of-use (TOCTOU) Race Condition)
-https://en.wikipedia.org/wiki/Time_of_check_to_time_of_use
+(** This module implements a check for CWE-367: Time-of-check Time-of-use (TOCTOU) Race Condition.
+
+    Time-of-check Time-of-use race conditions happen when a property of a resource
+    (e.g. access rights of a file) get checked before the resource is accessed, leaving
+    a short time window for an attacker to change the entity and thus invalidating
+    the check before the access.
+
+    See {: https://cwe.mitre.org/data/definitions/367.html} for a detailed description.
+
+    {1 How the check works}
+
+    For pairs of (check-call, use-call), configurable in config.json, we check whether
+    a function may call the check-call before the use-call.
+
+    {1 False Positives}
+
+    - The check-call and the use-call may access different, unrelated resources
+    (e. g. different files).
+
+    {1 False Negatives}
+
+    - If the check-call and the use-call happen in different functions it will not
+      be found by the check.
 *)
+
 val name : string
 val version : string
 

src/checkers/cwe_426.mli

-(** This module checks for CWE-426 (Untrusted Search Path) (https://cwe.mitre.org/data/definitions/426.html). Basically, the program searches
-for critical resources on an untrusted search path that can be adjusted by an adversary. For example, see Nebula Level 1
-(https://exploit-exercises.com/nebula/level01/).
-
-According to "man system" the following problems can arise:
-"Do not use system() from a program with set-user-ID or set-group-ID privileges, because strange values for some environment variables might
-be used to subvert system integrity.  Use the exec(3) family of functions instead, but not execlp(3) or execvp(3).  system() will not, in
-fact, work properly from programs with set-user-ID or set-group-ID privileges on systems on which /bin/sh is bash version 2, since bash 2
-drops privileges on startup.  (Debian uses a modified bash which does not do this when invoked as sh.)"
+(** This module implements a check for CWE-426: Untrusted Search Path.
+
+    Basically, the program searches for critical resources on an untrusted search
+    path that can be adjusted by an adversary. For example, see Nebula Level 1
+    ({: https://exploit-exercises.com/nebula/level01/}).
+
+    According to the manual page of system() the following problems can arise:
+    "Do not use system() from a program with set-user-ID or set-group-ID privileges,
+    because strange values for some environment variables might be used to subvert
+    system integrity.  Use the exec(3) family of functions instead, but not execlp(3)
+    or execvp(3).  system() will not, in fact, work properly from programs with set-user-ID
+    or set-group-ID privileges on systems on which /bin/sh is bash version 2, since bash 2
+    drops privileges on startup. (Debian uses a modified bash which does not do this when invoked as sh.)"
+
+    See {: https://cwe.mitre.org/data/definitions/426.html} for a detailed description.
+
+    {1 How the check works}
+
+    We check whether a function that calls a privilege-changing function (configurable
+    in config.json) also calls system().
+
+    {1 False Positives}
+
+    - If the call to system() happens before the privilege-changing function, the call
+    may not be used for privilege escalation
+
+    {1 False Negatives}
+
+    - If the calls to the privilege-changing function and system() happen in different
+    functions, the calls will not be flagged as a CWE-hit.
+    - This check only finds potential privilege escalation bugs, but other types of
+    bugs can also be triggered by untrusted search paths.
 *)
+
 val name : string
 val version : string
 

src/checkers/cwe_457.mli

-(** This module implements a check for CWE-457 (Use of Uninitialized Variable).
-TODO
-See https://cwe.mitre.org/data/definitions/457.html for detailed description. *)
+(** This module implements a check for CWE-457: Use of Uninitialized Variable.
+
+    Accessing variables on the stack or heap before their initialization can lead
+    to unintended or undefined behaviour, which could be exploited by an attacker.
+
+    See {: https://cwe.mitre.org/data/definitions/457.html} for a detailed description.
+
+    {1 How the check works}
+
+    The check uses the frame pointer to look for loads to addresses which do not
+    have an associated store instruction.
+
+    {1 False Positives}
+
+    - The check is still very basic and can be easily get confused by loads/stores
+    through different registers than the frame pointer.
+    - Modern compilers often use only the stack pointer for stack access, freeing
+    up the frame pointer as a general purpose register. This is not recognized by
+    the check.
+
+    {1 False Negatives}
+
+    - Heap accesses are not examined by the check.
+    - Memory accesses through different registers than the frame pointer are not
+    examined by the check.
+*)
+
 val name: string
 val version : string
 

src/checkers/cwe_467.mli

-(** This module implements a check for CWE-467 (Use of sizeof() on a Pointer Type).
-In a nutshell, it before a function call to symbols like malloc and memmove, which
-take a size parameter and a pointer to data as input, if not accidentally the size
-of the pointer instead of the data is passed. This can have severe consequences.
-The check is quite basic: it checks if before the call an immediate value that
-equals the size of a pointer (e.g. 4 bytes on x86) is referenced (e.g. pushed
-onto the stack).The symbols are configurable in config.json.
-See https://cwe.mitre.org/data/definitions/467.html for detailed description. *)
+(** This module implements a check for CWE-467: Use of sizeof() on a Pointer Type.
+
+    Functions like malloc and memmove take a size parameter of some data size as
+    input. If accidentially the size of a pointer to the data instead of the size of
+    the data itself gets passed to the function, this can have severe consequences.
+
+    See {: https://cwe.mitre.org/data/definitions/467.html} for a detailed description.
+
+    {1 How the check works}
+
+    The check is quite basic: We check whether in the basic block before a call
+    to a function listed in the symbols for CWE467 (configurable in in config.json)
+    an immediate value that equals the size of a pointer (e.g. 4 bytes on x86) is
+    referenced.
+
+    {1 False Positives}
+
+    - It is not checked whether the immediate value is actually an input to the call
+    or not. However, this does not seem to produce false positives in practice.
+    - The size value might be correct and not a bug.
+
+    {1 False Negatives}
+
+    - If the incorrect size value is generated before the basic block that contains
+      the call, the check will not be able to find it.
+*)
+
 val name : string
 val version : string
 

src/checkers/cwe_476.mli

-(** This module implements a check for CWE-476 (NULL Pointer Dereference).
-    It checks if the result of a function that may return a NULL value is checked
-    for NULL before any memory gets accessed using the return values. The symbols
-    are configurable in config.json. See https://cwe.mitre.org/data/definitions/476.html
-    for detailed description.
-
-    Parameters:
-    - strict_call_policy={true, false}: Determines behaviour on call and return instructions.
+(** This module implements a check for CWE-476: NULL Pointer Dereference.
+
+    Functions like malloc() may return NULL values instead of pointers to indicate
+    failed calls. If one tries to access memory through this return value without
+    checking it for being NULL first, this can crash the program.
+
+    See {: https://cwe.mitre.org/data/definitions/476.html} for a detailed description.
+
+    {1 How the check works}
+
+    We search for an execution path where a memory access using the return value of
+    a symbol happens before the return value is checked through a conditional
+    jump instruction.
+
+    Note that the check relies on Bap-generated stubs to identify return registers of the
+    checked functions. Therefore it only works for functions for which Bap generates
+    these stubs.
+
+    {2 Parameters configurable in config.json}
+
+    - strict_call_policy=\{true, false\}: Determines behaviour on call and return instructions.
       If false, we assume that the callee, resp. the caller on a return instruction,
       checks all unchecked values still contained in the registers. If true, every
       unchecked value on a call or return instruction gets reported.
     - max_steps=<num>: Max number of steps for the dataflow fixpoint algorithm.
 
-    Notes: The check relies on Bap-generated stubs to identify return registers of the
-    checked functions. Therefore it only works for functions for which Bap generates
-    these stubs. *)
+    {2 Symbols configurable in config.json}
+
+    The symbols are the functions whose return values are assumed to be potential
+    NULL pointers.
+
+    {1 False Positives}
+
+    - The check does not yet track values on the stack. Thus instances, where the
+    return value gets written onto the stack before the check happens get incorrectly
+    flagged. This happens a lot on unoptimized binaries but rarely on optimized ones.
+
+    {1 False Negatives}
+
+    - We do not check whether an access to a potential NULL pointer happens regardless
+    of a prior check.
+    - We do not check whether the conditional jump instruction checks specifically
+    for the return value being NULL or something else
+    - For functions with more than one return value we do not distinguish between
+    the return values.
+*)
 
 val name : string
 val version : string

src/checkers/cwe_560.mli

-(** CWE-560 (Use of umask() with chmod-style Argument)
-https://cwe.mitre.org/data/definitions/560.html
-
-The program uses the system call umask(2) with arguements for chmod(2). For instance,
-instead of a reasonable value like 0022 a value like 0666 is passed. This may result wrong
-read and/or write access to files and directories, which could be utilized to bypass
-protection mechanisms.
-
-This check looks for umask calls and checks if they have a reasonable value, i.e. smaller than
-a certain value, currently set to 1000 and greater than a reasonable value for umask, currently set to 100.
-A future version should include a proper data flow analysis to track the first argument since the current
-version considers all immediate values of an umask callsite's basic block.
+(** This module implements a check for CWE-560: Use of umask() with chmod-style Argument.
+
+    The program uses the system call umask(2) with arguements for chmod(2). For instance,
+    instead of a reasonable value like 0022 a value like 0666 is passed. This may result wrong
+    read and/or write access to files and directories, which could be utilized to bypass
+    protection mechanisms.
+
+    See {: https://cwe.mitre.org/data/definitions/560.html} for a detailed description.
+
+    {1 How the check works}
+
+    This check looks for umask calls and checks if they have a reasonable value, i.e. smaller than
+    a certain value, currently set to 1000 and greater than a reasonable value for umask, currently set to 100.
+
+    {1 False Positives}
+
+    - The current version considers all immediate values of an umask callsite's basic
+    block. It does not check whether the value is an input to the call or not.
+
+    {1 False Negatives}
+
+    - If the input to umask is not defined in the basic block before the call, the
+    check will not see it.
+    - Calls where the input is not an immediate value but a variable are not examined.
 *)
+
 val name : string
 val version : string
 

src/checkers/cwe_676.mli

-(** This module implements a check for CWE-676 (Use of Potentially Dangerous Function)
-Potentially dangerous functions like memcpy can lead to security issues like buffer overflows.
-The functions are configurable in config.json.
-See https://cwe.mitre.org/data/definitions/676.html for detailed description. *)
+(** This module implements a check for CWE-676: Use of Potentially Dangerous Function.
+
+    Potentially dangerous functions like memcpy can lead to security issues like buffer
+    overflows.
+
+    See {: https://cwe.mitre.org/data/definitions/676.html} for a detailed description.
+
+    {1 How the check works}
+
+    Calls to dangerous functions are flagged. The list of functions that are considered
+    dangerous can be configured in config.json. The default list is taken from
+    {: https://github.com/01org/safestringlib/wiki/SDL-List-of-Banned-Functions}.
+
+    {1 False Positives}
+
+    None known
+
+    {1 False Negatives}
+
+    None known
+*)
+
 val name : string
 val version : string
 

src/checkers/cwe_782.mli

-(** TODO
-CWE-782 (Exposed IOCTL with Insufficient Access Control)
-https://cwe.mitre.org/data/definitions/782.html *)
+(** This module implements a check for CWE-782: Exposed IOCTL with Insufficient Access Control.
+
+    See {: https://cwe.mitre.org/data/definitions/782.html} for a detailed description.
+
+    {1 How the check works}
+
+    Calls to ioctl() get flagged as CWE hits.
+
+    {1 False Positives}
+
+    - We cannot check whether the call contains sufficient access control.
+
+    {1 False Negatives}
+
+    - There are other ways to expose I/O control without access control.
+*)
+
 val name : string
 val version : string
 

src/config.json

@@ -3,7 +3,8 @@
     "symbols": [
       "xmalloc",
       "malloc",
-      "realloc"
+      "realloc",
+      "calloc"
     ]
   },
   "CWE215": {

src/cwe_checker_core.opam

@@ -18,6 +18,7 @@ depends: [
   "bap" {>= "1.6"}
   "core_kernel" {>= "v0.11" & < "v0.12"}
   "ppx_jane" {>= "v0.11" & < "v0.12"}
+  "odoc" {>= "1.4"}
 ]
 depexts: [
   "binutils"