 |
Systems Analysis & Verification
F-Soft Publications
F-Soft Overview
Introduction
F-Soft is a platform for verifying source code programs. It can check
C programs for runtime errors:
- Pointer access violations,
- Static/dynamic buffer overflows,
- Memory leaks,
- Standard C library API usage (including C string null termination)
- Other user-defined properties (type-state verification)
It can be used to check programs globally, or it can be used as
an annotation checker for checking user written contracts. We
have successfully analyzed large benchmark examples to find previously
unknown bugs using F-Soft [1]. An in-house product
based on F-Soft, called VARVEL, is currently in use at
NEC.
The input C program is parsed using a custom-built front end (including
CIL)
that performs pointer analysis, heap modeling, slicing, constant
folding and numerous simplifications to construct a control flow
graph (CFG) model of the program. It safely handles many of the
complications in the C language such as pointer arithmetic and pointer
aliasing for both heap and stack memory. It has support for bounded
modeling of arrays and recursive heap data structures. These modeling
details and automatic instrumentation for standard runtime errors are
described in
[1, 2, 3].
Static Analysis Engines
F-Soft employs a powerful static analysis engine
to prove properties. We employ
flow, context sensitive and partially path-sensitive static analysis
using abstract interpretation on abstract domains of increasing
precision. These include intervals , octagons,
symbolic ranges[5], and
polyhedra. The properties proved by these analyses are sliced away
from the CFG, which is used for verifying the remaining properties
by model checking. Invariants
generated by these static analyses are also utilized by model checking
to improve scalability. Details of static analyses used in F-Soft can
be found in [1, 4, 5, 6].
Model Checking Engines
The sliced model after static analysis is bit-blasted to construct a
bit-accurate FSM model of the program for model checking the remaining
properties. Information from range analysis is used to reduce the
bit-widths of variables in this model [7]. For model checking, we can
use a variety of bounded and unbounded model checking techniques for
finding bugs as well as proofs. These back-end techniques are provided
by the VeriSol model checking platform [8] (additional details in
[9]). For software verification, we mainly use SAT-based techniques [2, 3] to find bugs or proofs. A word-level verification model (after suitable linearizing abstractions) can also be derived, for verification by SMT-based BMC [10] or polyhedra-based unbounded model checking
[11]. The key advantage of using a model checker is that it provides
concrete counterexamples to help understand and fix the bugs that it
discovers. These counterexamples can also be used to improve the
accuracy of abstraction during static analysis.
Debugging
Finally, we utilize the generated counterexamples to generate reproducible bug traces for the user to inspect. We support a HTML-based debugging interface that allows the user to visualize multiple reported bugs by tracing the source code and the whole path of the trace or the important parts of the discovered bug path. Furthermore, we also generate an appropriate environment model that can be compiled with the source code to generate an executable of the bug allowing the user to utilize common debuggers such as gdb on the reproducible witness path.
Integration of Static Analysis and Model Checking
The integrated platform for static analyses and model checking in
F-Soft provides many opportunities for combining the scalability of
the former with the accuracy of the latter.
For example, we use invariants generated by abstract interpretation to improve the
performance of SMT-based BMC [10]. We have also used these invariants
to avoid expensive refinement steps in predicate abstraction
refinement [12].
Another example is a tighter integration
between static analysis and model checking based on polyhedra [13],
where the precision of the abstract reachability analysis is improved
by using concrete counterexamples.
Current Directions
We are currently exploring techniques for automatic specification
inference [14, 15] to assist
in applying F-Soft to check interface contracts, or to provide
interface environment models to the tool. Other interesting directions
including symbolic execution [16], modular
verification, and handling multi-threaded programs as a part of a
separate project called ConSave. We are also focussing on
embedded systems, especially for automotive/avionic domains, as a part of a related
project called TeSSa.
Other Information
A description of the Varvel tool from NEC is
available
here.
F-Soft Important References
[1] Franjo Ivančić, Sriram Sankaranarayanan, Ilya Shlyakhter, and Aarti Gupta. Buffer Overflow Detection for Large C Programs using Environment Refinement. Unpublished manuscript.
[2] Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav Ashar. Efficient SAT-based Bounded Model Checking for Software Verification, Journal on Theoretical Computer Science (TCS), Volume 404(3), September 2008, pages 256-274.
[3] F. Ivancic, I. Shlyakhter, A. Gupta, M. Ganai, V. Kahlon, C. Wang, Z. Yang. Model Checking C Programs Using F-Soft, in Proceedings of the International Conference on Computer Design (ICCD), October 2005.
[4] Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static Analysis in Disjunctive Numerical Domains . In Proceedings of the International Static Analysis Symposium (SAS), August 2006.
[5] Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta: Program Analysis Using Symbolic Ranges. SAS 2007: 366-383
[6] G. Balakrishnan, S. Sankaranarayanan, F. Ivancic, O. Wei, and A. Gupta, SLR: Path-Sensitive Analysis Through Infeasible-Path Detection and Syntactic-Language Refinement. In Proceedings of the International Static Analysis Symposium (SAS), July 2008.
[7] Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivančić, Srihari Cadambi, Malay K. Ganai, Aarti Gupta, and Pranav Ashar. Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking, Transactions Brief Paper in the IEEE Transactions on CAD, volume 27(8), Aug. 2008, pages 1513-1517.
[8] M. K. Ganai, A. Gupta, and P. Ashar. SAT-based Model Checking Platform for Large Scale Systems, in Proceedings of Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2005.
[9] A. Gupta, M. K. Ganai, and C. Wang. SAT-based Verification Methods and Applications in Hardware Verification. In School for Formal Methods (SFM06:HV), LNCS Vol. 3965, May 2006.
[10] M. K. Ganai and A. Gupta. Accelerating High-level Bounded Model Checking . In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD), November 2006.
[11] Z. Yang, C. Wang, A. Gupta, and F. Ivancic. Mixed Symbolic Representations for Model Checking Software Programs . In Proceedings of the ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2006.
[12] H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, and C. Wang. Using statically computed invariants inside the predicate abstraction and refinement loop. In Proceedings of the International Conference on Computer Aided Verification (CAV), August 2006.
[13] C. Wang, Z. Yang, A. Gupta, and F. Ivancic. Using counterexamples for improving the precision of reachability computation with polyhedra. In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2007.
[14] Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivančić, and Aarti Gupta. Dynamically Inferring Likely Data Preconditions over Predicates by Tree Learning, in Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), Seattle, WA, July 2008.
[15] Sankaranarayanan, Franjo Ivančić, and Aarti Gupta. Mining Library Specifications using Inductive Logic Programming, in Proceedings of the International Conference on Software Engineering (ICSE), Leipzig, Germany, May 2008.
[16] Nishant Sinha. Symbolic Program Analysis using Term Rewriting and Generalization, in Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), November 2008 (To Appear).
F-Soft References by Year
2009
Z. Yang, C. Wang, A. Gupta and F. Ivancic.
Model Checking Sequential Software Programs Via Mixed Symbolic Analysis.
ACM TODAES 13(1), January 2009.
Malay K. Ganai and Weihong Li.
Bang for the Buck: Improvising and Scheduling Verification Engines for Effective Resource Utilization.
Memocode, Boston. July 2009.
Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta
Refining the Control Structure of Loops using Static Analysis
EMSOFT09, Grenoble, France, Oct 09.
Franjo Ivancic, Sriram Sankaranarayanan, Aarti Gupta and Ilya Shlyakhter,
Buffer Overflow Analysis using Environment Refinement, Draft
[PDF]
2008
N. Sinha,
Symbolic Program Analysis Using Term Rewriting and Generalization,
In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD),
November 2008, Portland, OR, USA. [Slides]
G. Balakrishnan, S. Sankaranarayanan, F. Ivancic, O. Wei, and A. Gupta,
SLR: Path-Sensitive Analysis Through Infeasible-Path Detection and Syntactic-Language Refinement.
In Proc. Static Analysis Symposium (SAS), July 2008.
Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Nadia Papakonstantinou, Sriram Sankaranarayanan, and Chao Wang:
Towards Precise and Scalable Verification of Embedded Software,
In Proceedings of 2008 Design and Verification Conference (DVCon), San Jose, CA, February 2008.
2007
C. Wang, A. Gupta, and F. Ivancic:
Induction in CEGAR for Detecting Counterexamples.
In Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD), November 2007.
F. Ivancic, Z. Yang, M.K. Ganai, A. Gupta, and P. Ashar.
Efficient SAT-based Bounded Model Checking for Software Verification.
In Journal on Theoretical Computer Science (TCS), accepted for publication.
S. Sankaranarayanan, F. Ivancic, and A. Gupta.
Program analysis using symbolic ranges.
In Proceedings of the International Static Analysis Symposium (SAS), August 2007.
C. Wang, Z. Yang, A. Gupta, and F. Ivancic.
Using counterexamples for improving the precision of reachability computation with polyhedra.
In Proceedings of the International Conference on Computer Aided Verification (CAV), July 2007.
2006
C. Wang, Z. Yang, F. Ivancic, and A. Gupta.
Whodunit? Causal Analysis for Counterexamples.
In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA), September 2006.
S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta.
Static Analysis in Disjunctive Numerical Domains .
In Proceedings of the International Static Analysis Symposium (SAS), August 2006.
A. Zaks, I. Shlyakhter, F. Ivancic, S. Cadambi, Z. Yang, M. K. Ganai, A. Gupta, and P. Ashar.
Using Range Analysis for Software Verification.
In International Workshop on Software Verification and Validation (SVV), August 2006.
H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, and C. Wang.
Using statically computed invariants inside the predicate abstraction and refinement loop.
In Proceedings of the International Conference on Computer Aided Verification (CAV), August 2006.
2005
F. Ivancic, I. Shlyakhter, A. Gupta, M. Ganai, V. Kahlon, C. Wang, Z. Yang.
Model Checking C Programs Using F-Soft,
in Proceedings of the International Conference on Computer Design (ICCD), October 2005.
V. Kahlon, F. Ivancic, A. Gupta.
Reasoning about threads communicating via locks,
in Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.
F. Ivancic, Z. Yang, M. Ganai, A. Gupta, I. Shlyakhter, P. Ashar.
F-Soft: Software Verification Platform,
in Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005.
H. Jain, F. Ivancic, A. Gupta, M. Ganai.
Localization and Register Sharing for Predicate Abstraction ,
in Proceedings of Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2005.
2004
F. Ivancic, Z. Yang, M. Ganai, A. Gupta, P. Ashar.
Efficient SAT-based Bounded Model Checking for Software Verification ,
Presented at International Symposium for Leveraging Applications of Formal Methods (ISoLA) 2004.
Publications in Other Areas:
|
