Overview

We develop Weak-Assert, a weakness-oriented assertion recommendation tool kit for program analysis. Our target is ordinary C programs. Weak-Assert applies to several types of program weaknesses, which are classified in Common Weakness Enumeration (CWE).

Weak-Assert uses well-designed patterns (such as CWE134, CWE195, etc) to match the abstract syntax trees of source code automatically. It collects significant messages(such as variable names, line numbers, etc) from trees and insert assertions into proper locations of programs. These assertions can be checked by using program analysis techniques, such as program testing and verification.

In short, Weak-Assert needs a C source file and specified CWE types as input. Automatically, Weak-Assert insert weakness-oriented assertions (if needed) into the source code and finally produce a new file, which can be used to test or verify. We package Weak-Assert as a tool kit, which can be used in command line conveniently.

Framework

Weak-Assert is a command line tool implemented in Python language on Ubuntu 16.04. It depends on libClang to parse C code into abstract syntax tree. The framework is shown in the picture above. It contains three modules: input processing module, code parsing module and assertion recommend module.

Firstly, The initial parameters of the execution are set in input processing module. Users are able to apply Weak-Assert to a directory (entrance of C language projects) or a single source file. Program weakness types also can be chosen. Weak-Assert support six different types of common weakness (ID.134,195,674,690,789,835), which are well defined in CWE (Common Weakness Enumeration). Besides, users can choose to verify the assertions inserted by Weak-Assert. We use an open source program verification tool, smack, to verify the assertions.

In code parsing module, Weak-Assert integrate libClang, which provides a C interface to abstract syntax tree. The abstract syntax tree is filtered to remove those which are included from other files (no matter source files or head files).

In assertion recommend module, Weak-Assert matches the abstract syntax trees with designed patterns, which are corresponding to supported weaknesses. Through traversing the entire tree, we capture the weakness types, locations and variable names. Then Weak-Assert inserts assertions to generate new files. These assertions are inserted into specified locations in order to be detected before the weaknesses are triggered. Finally if users want to verify the assertions, which are recommended, Weak-Assert is able to call Smack to finish the formal program verification tasks automatically.

©2017 wangcong15@mails.tsinghua.edu.cn