CIL to Java']Java-bytecode Translation for Static Analysis Leveraging

被引：2
|
作者：
Ferrara, Pietro [1 ]
Cortesi, Agostino [2 ]
Spoto, Fausto [3 ]
机构：
[1] JuliaSoft SRL, Verona, Italy
[2] Univ Ca Foscari Venezia, Venice, Italy
[3] Univ Verona, Verona, Italy
来源：
2018 ACM/IEEE CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE 2018) | 2018年
关键词：
D O I：
10.1145/3193992.3193994
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. The overall process of translation and analysis is fast, scales up to industrial programs, and introduces a negligible number of false alarms. The main result of this work is to leverage existing, mature, and sound analyzers for Java bytecode by applying them to the (translated) CIL bytecode.
引用
收藏
页码：40 / 49
页数：10
相关论文
共 50 条
  • [31] An Efficient, Parametric Fixpoint Algorithm for Analysis of Java']Java Bytecode
    Mendez, Mario
    Navas, Jorge
    Hermenegildo, Manuel V.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 190 (01) : 51 - 66
  • [32] Magic-sets transformation for the analysis of Java']Java bytecode
    Payet, Etienne
    Spot, Fausto
    STATIC ANALYSIS, PROCEEDINGS, 2007, 4634 : 452 - +
  • [33] Verified Java']Java Bytecode Verification
    Klein, Gerwin
    IT-INFORMATION TECHNOLOGY, 2005, 47 (02): : 107 - 110
  • [34] Java']Java & static analysis
    Chaturvedi, A
    DR DOBBS JOURNAL, 2005, 30 (07): : 25 - +
  • [35] Experiments with Non-Termination Analysis for Java']Java Bytecode
    Payet, Etienne
    Spoto, Fausto
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 253 (05) : 83 - 96
  • [36] Runtime Input Validation for Java']Java Web Applications using Static Bytecode Instrumentation
    Cho, Sangwook
    Kim, Gyoosik
    Cho, Seong-je
    Choi, Jongmoo
    Park, Minkyu
    Han, Sangchul
    2016 RESEARCH IN ADAPTIVE AND CONVERGENT SYSTEMS, 2016, : 148 - 152
  • [37] An Evaluation of Current Java']Java Bytecode Decompilers
    Hamilton, James
    Danicic, Sebastian
    2009 NINTH IEEE INTERNATIONAL WORKING CONFERENCE ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2009, : 129 - 136
  • [38] Vulnerabilities Constraint Based Analysis Approach for Java']Java Bytecode Programs
    Achour, Safaa
    Benattou, Mohammed
    PROCEEDINGS OF 2018 6TH INTERNATIONAL CONFERENCE ON MULTIMEDIA COMPUTING AND SYSTEMS (ICMCS), 2018, : 93 - 98
  • [39] Using CLP Simplifications to Improve Java']Java Bytecode Termination Analysis
    Spoto, Fausto
    Lu, Lunjin
    Mesnard, Fred
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 253 (05) : 129 - 144
  • [40] Verification of Java']Java bytecode using analysis and transformation of logic programs
    Albert, E.
    Gomez-Zamalloa, M.
    Hubert, L.
    Puebla, G.
    PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, 2007, 4354 : 124 - +
12345