Static analysis by abstract interpretation: application to the detection of heap overflows

被引：4
作者：
Allamigeon, Xavier [1 ,2 ]
Hymans, Charles [1 ]
机构：
[1] EADS Innovat Works, SE CS, Suresnes, France
[2] CEA, LIST MeASI, Gif Sur Yvette, France
来源：
JOURNAL OF COMPUTER VIROLOGY AND HACKING TECHNIQUES | 2008年 / 4卷 / 01期
关键词：
D O I：
10.1007/s11416-007-0063-z
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Several security flaws are the consequence of the presence of programming errors or bugs in software. Heap overflow is the typical example of such errors that allows an attacker to take control of a machine. But considering the growing size and complexity of present software, implementing programs without any error is not an easy task. In this paper, we present a static analysis by abstract interpretation that is focused on security properties: without executing the program, it ensures the absence of any heap overflows.
引用
收藏
页码：5 / 23
页数：19
相关论文
共 40 条
[1]  
Allamigeon X, 2006, LECT NOTES COMPUT SC, V4134, P35
[2]  
Ball T, 2004, LECT NOTES COMPUT SC, V2988, P388
[3]   A static analyzer for large safety-critical software [J].
Blanchet, B ;
Cousot, P ;
Cousot, R ;
Feret, J ;
Mauborgne, L ;
Miné, A ;
Monniaux, D ;
Rival, X .
ACM SIGPLAN NOTICES, 2003, 38 (05) :196-207
[4]   An efficient cryptographic protocol verifier based on prolog rules [J].
Blanchet, B .
14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, :82-96
[5]   A computationally sound mechanized prover for security protocols [J].
Blanchet, Bruno .
2006 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, PROCEEDINGS, 2006, :140-154
[6]   Improving computer security using extended static checking [J].
Chess, BV .
2002 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, PROCEEDINGS, 2002, :160-173
[7]   MODEL CHECKING AND ABSTRACTION [J].
CLARKE, EM ;
GRUMBERG, O ;
LONG, DE .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (05) :1512-1542
[8]   AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].
CLARKE, EM ;
EMERSON, EA ;
SISTLA, AP .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263
[9]  
Clarke EM, 1999, MODEL CHECKING, P1
[10]   CONSTRUCTIVE VERSIONS OF TARSKI FIXED-POINT THEOREMS [J].
COUSOT, P ;
COUSOT, R .
PACIFIC JOURNAL OF MATHEMATICS, 1979, 82 (01) :43-57
1234