Hassen Saïdi
Abstract
Static analysis has emerged in recent years as an indispensable tool in software verification. Unlike deductive approaches to program verification, static analysis can only prove simple properties. Moreover, the myriad of static analysis tools employ specific techniques that target specific properties of specific programs. Static analysis holds the promise of complete automation, scalability, and handling larger classes of properties and larger classes of systems, but a significant gap exists between such a goal and current static analysis tools. We argue that a logical foundation for static analysis allows the construction of more powerful static analysis tools that are provably correct, extensible, and interoperable, and can guarantee more complex properties of complex systems. We address these challenges by proposing a tool-bus architecture that allows the combination of several static analysis tools and methods. The combination is achieved at the logical level using decision procedures that implement combination of theories. We discuss the application of such ideas to binary program analysis in the context of intrusion detection and malware analysis.
- IDA Pro Dissasember. http://www.datarescue.com/ida.htm.Google Scholar
- G. Balakrishnan and T. Reps. Analyzing memory accesses in x86 executables. In Proc. Compiler Construction (LNCS 2985), pages 5--23. Springer Verlag, Apr. 2004.Google ScholarCross Ref
- T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1--3, Jan. 2002. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Symposium on Principles of Programming Languages, pages 238--252. ACM Press, Jan. 1977. Google ScholarDigital Library
- B. Dutertre and L. de Moura. A fast linear-arithmetic solver for dpll(t). In The 18th Computer-Aided Verification Conference (CAV'06), Seattle, June 2006. Lecture Notes in Computer Science. Google ScholarDigital Library
- M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2): 1--25, Feb. 2001. Google ScholarDigital Library
- S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 72--83, Haifa, Israel, June 1997. Springer Verlag. Google ScholarDigital Library
- S. Gulwani and A. Tiwari. Combining abstract interpreters. In PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pages 376--386, New York, NY, USA, 2006. ACM Press. Google ScholarDigital Library
- W. McCloskey, S. Gulwani, and A. Tiwari. Lifting abstract interpreters to quantified abstract domains. In Proc. Principles of Programming Languages, POPL, 2008. To appear. Google ScholarDigital Library
- S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607, pages 748--752. Springer Verlag, June 1992. Google ScholarDigital Library
- H. Saïdi. Guarded models for intrusion detection. In PLAS '07: Proceedings of the 2007 workshop on Programming languages and analysis for security, pages 85--94, New York, NY, USA, 2007. ACM Press. Google ScholarDigital Library
- A. Tiwari and S. Gulwani. Logical interpretation: Static program analysis using theorem proving. In F. Pfenning, editor, CADE-21, volume 4603 of LNAI, pages 147--166. Springer, 2007. Google ScholarDigital Library
- P. Vales, J. Butler, D. Rager, C. Stack, and C. Telfer. Gaps in static analysis tools coverage. In OMGs First Software Assurance Workshop: Working Together for Confidence, Fairfax, VA, mar 2007.Google Scholar
Index Terms
- Logical foundation for static analysis: application to binary static analysis for security
Recommendations
Combined Static and Dynamic Analysis
Static analysis is usually faster than dynamic analysis but less precise. Therefore it is often desirable to retain information from static analysis for run-time verification, or to compare the results of both techniques. However, this requires writing ...
Integrated Static and Dynamic Analysis for Malware Detection
AbstractThe number of malware is increasing rapidly regardless of the common use of anti-malware software. Detection of malware continues to be a challenge as attackers device new techniques to evade from the detection methods. Most of the anti-virus ...
Optimistic Hybrid Analysis: Accelerating Dynamic Analysis through Predicated Static Analysis
ASPLOS '18Dynamic analysis tools, such as those that detect data-races, verify memory safety, and identify information flow, have become a vital part of testing and debugging complex software systems. While these tools are powerful, their slow speed often limits ...
Comments