Completeness of Abstract Domains for String Analysis of Java']JavaScript Programs

被引:6
作者
Arceri, Vincenzo [1 ]
Olliaro, Martina [2 ,3 ]
Cortesi, Agostino [2 ]
Mastroeni, Isabella [1 ]
机构
[1] Univ Verona, Verona, Italy
[2] Ca Foscari Univ Venice, Venice, Italy
[3] Masaryk Univ Brno, Brno, Czech Republic
来源
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2019 | 2019年 / 11884卷
关键词
String abstract domains; Abstract interpretation completeness; String analysis; STATIC ANALYSIS; SMT SOLVER;
D O I
10.1007/978-3-030-32505-3_15
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Completeness in abstract interpretation is a well-known property, which ensures that the abstract framework does not lose information during the abstraction process, with respect to the property of interest. Completeness has been never taken into account for existing string abstract domains, due to the fact that it is difficult to prove it formally. However, the effort is fully justified when dealing with string analysis, which is a key issue to guarantee security properties in many software systems, in particular for JavaScript programs where poorly managed string manipulating code often leads to significant security flaws. In this paper, we address completeness for the main JavaScript-specific string abstract domains, we provide suitable refinements of them, and we discuss the benefits of guaranteeing completeness in the context of abstract-interpretation based string analysis of dynamic languages.
引用
收藏
页码:255 / 272
页数:18
相关论文
共 39 条
[31]   The 4-Octahedron Abstract Domain [J].
Oucheikh, Rachid ;
Berrada, Ismail ;
El Hichami, Outman .
Networked Systems, NETYS 2016, 2016, 9944 :311-317
[32]  
Park S, 2016, 2016 IEEE/ACM 4TH INTERNATIONAL WORKSHOP ON SOFTWARE ENGINEERING FOR SYSTEMS-OF-SYSTEMS (SESOS), P25, DOI [10.1145/2897829.2897834, 10.1109/SESoS.2016.013]
[33]   A Symbolic Execution Framework for Java']JavaScript [J].
Saxena, Prateek ;
Akhawe, Devdatta ;
Hanna, Steve ;
Mao, Feng ;
McCamant, Stephen ;
Song, Dawn .
2010 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, 2010, :513-528
[34]  
Se-Won Kim, 2014, Programming Languages and Systems. 12th Asian Symposium (APLAS 2014), Proceedings: LNCS 8858, P372, DOI 10.1007/978-3-319-12736-1_20
[35]  
Veanes Margus, 2010, Proceedings of the Third IEEE International Conference on Software Testing, Verification and Validation (ICST 2010), P498, DOI 10.1109/ICST.2010.15
[36]   The closure operators of a lattice [J].
Ward, M .
ANNALS OF MATHEMATICS, 1942, 43 :191-196
[37]   Sound and Precise Analysis of Web Applications for Injection Vulnerabilities [J].
Wassermann, Gary ;
Su, Zhendong .
PLDI'07: PROCEEDINGS OF THE 2007 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2007, :32-41
[38]  
Yu F, 2008, LECT NOTES COMPUT SC, V5156, P306
[39]   Automata-based symbolic string analysis for vulnerability detection [J].
Yu, Fang ;
Alkhalaf, Muath ;
Bultan, Tevfik ;
Ibarra, Oscar H. .
FORMAL METHODS IN SYSTEM DESIGN, 2014, 44 (01) :44-70