Department of Systems Analysis & Verification - PROJECTS

NEC Laboratories America, Inc., Princeton Campus

Currently, we have the following active ongoing projects:

- ConSave: Analysis and verification for concurrent systems and programs
- F-Soft: A software analysis framework for C programs
- Tessa: Techniques for Embedded System and Software Assurance
- VeriSol: A SAT-based model checking tool for digital circuits.

F-Soft

F-Soft is an analyzer for commercial C programs. It can check C programs for runtime memory safety issues such as pointer access violations, buffer overflow, memory leaks , standard library API usage and other user defined properties. The tool can be used to check programs globally or as an annotation checker for checking user written contracts. The F-Soft tool flow utilizes both model checking techniques to find concrete bugs and abstract interpretation techniques for proofs. We have successfully analyzed large benchmark examples to find previously unknown bugs using the F-Soft tool.

The input C program is parsed using a custom built front end that performs pointer analysis, heap modelling, slicing, constant folding and numerous simplifications to construct a CFG model of the program. Our model is interprocedural. It safely handles many of the complications in the C language such as pointer arithmetic and aliasing for both heap and stack memory. It has support for bounded modelling of arrays and recursive heap data structures.

The front end also uses a powerful static analysis engine to prove properties. We employ flow, context sensitive and partially path-sensitive static analysis. Abstract interpretation is then performed using many domains including intervals , octagons , symbolic ranges and polyhedra. The properties proved by these analyses are sliced away from the CFG. The remaining model is bit blasted to construct a boolean model of the program for model checking.

We use a combination of many SAT-based and high level model checking engines including VeriSol to model check the boolean model generated by our front end. The key advantage of using a model checker is that it provides concrete counter examples to help understand and fix the bugs that it discovers.

VeriSol

The objective of this project is to reduce hardware developments costs, to reduce hardware development cycle, and to increase the quality of hardware by applying formal analysis methods to find HW defects/bugs and proofs of correctness. We develop efficient and scalable model checking techniques at Boolean level (Bounded Model Checking, Abstraction-refinement, Efficient Memory Modeling), high performance constraint solvers (SAT solvers, high-level arithmetic solvers) and verification techniques at higher levels of design abstraction (e.g. word-level, arithmetic) for improving performance and scalability. We also investigate semi-formal verification techniques to combine benefits of formal techniques with simulation (SystemFV).

VeriSol is available commerically as a C-level property checker in CyberWorkBench (CWB), a System LSI Design Environment, developed and provided by NEC System Technologies, Ltd.