Symbolic approximation: an approach to verification in the large
Tóm tắt
This article describes symbolic approximation, a theoretical foundation for techniques evolved for large-scale verification – in particular, for post hoc verification of the C code in large-scale open-source projects such as the Linux kernel. The corresponding toolset’s increasing maturity means that it is now capable of treating millions of lines of C code source in a few hours on very modest support platforms. In order to explicitly manage the state-space-explosion problem that bedevils model-checking approaches, we work with approximations to programs in a symbolic domain where approximation has a well-defined meaning. A more approximate program means being able to say less about what the program does, which means weaker logic for reasoning about the program. So we adjust the approximation by adjusting the applied logic. That guarantees a safe approximation (one which may generate false alarms but no false negatives) provided the logic used is weaker than the exact logic of C. We choose the logic to suit the analysis.
Tài liệu tham khảo
Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Proc. POPL ’02: Proceedings of the ACM SIGPLAN-SIGACT conference on principles of programming languages
Breuer PT, Bowen JP (1995) A PREttier compiler–compiler: Generating higher order parsers in C. Softw Pract Exp 25(11):1263–1297
Breuer PT, Pickin S (2006) One million (Loc) and counting: static analysis for errors and vulnerabilites in the Linux kernel source code. In: Pinho LM, Harbour MG (eds) Proceedings of Reliable Software Technologies—Ada-Europe 2006, 11th Ada-Europe international conference on Reliable Software Technologies, Ser. LNCS, PP. 56–70
Breuer PT, Garcia Valls M (2004) Static deadlock detection in the Linux kernel. In: Llamosí A, Strohmeier A (eds) Reliable software technologies – Ada-Europe 2004, 9th Ada-Europe International Conference on Reliable Software Technologies, Palma de Mallorca, Spain, 14–18, June 2004. LNCS vol 3063. Springer, Berlin Heidelberg New York, pp 52–64
Breuer PT, Delgado Kloos C, Martínez Madrid N, López Marin A, Sánchez L (1997) A refinement calculus for the synthesis of verified digital or analog hardware descriptions in VHDL. ACM Trans Program Lang Syst (TOPLAS) 19(4):586–616
Breuer PT, Martínez Madrid N, Sánchez L, Marín A, Delgado Kloos C (1996) A formal method for specification and refinement of real-time systems. In: Proceedings of the 8th EuroMicro workshop on real time systems, IEEE, New York, L’aquilla, Italy, pp. 34–42
Chaki S, Clarke E, Groce A, Jha S, Veith H (2003) Modular verification of software components in C. In: Proceedings of the international conference on software engineering, pp. 385–389
Clarke E, Emerson E, Sistla A (1986) Automiatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Trans Program alang Syst 16(5):1512–1542
Clarke E, Grumberg O, Long D.A (1994) Model Checking and Abstraction. ACM Trans Program Lang Syst 16(5):1512–1542
Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM symposium on the principles of programming languages, pp 238–252
Chen H, Dean D, Wagner D (2004) Model checking one million lines of C code. In: Proceedings of the 11th annual network and distributed system security symposium, San Diego, CA
Foster JS, Fähndrich M, Aiken A (1999) A theory of type qualifiers. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI’99), Atlanta, Georgia
Foster JS, Terauchi T, Aiken A (2002) Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI’02), Berlin, Germany, pp 1–12
Johnson R, Wagner D (2004) Finding User/Kernel pointer bugs with type inference. In: Proceedings of the 13th USENIX security symposium, 9–13 August 2004, San Diego, CA, USA
Wagner D, Foster JS, Brewer EA, Aiken A (2000) A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of the network and distributed system security (NDSS) symposium, 2–4 February 2000, San Diego, CA, USA