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 条
  • [41] PicoJava']Java: A direct execution engine for Java']Java bytecode
    McGhan, H
    O'Connor, M
    COMPUTER, 1998, 31 (10) : 22 - +
  • [42] Advanced obfuscation techniques for Java']Java bytecode
    Chan, JT
    Yang, W
    JOURNAL OF SYSTEMS AND SOFTWARE, 2004, 71 (1-2) : 1 - 10
  • [43] Abstract Interpretation of Java']Java Bytecode in Sturdy
    Marx, Stefan
    Erdweg, Sebastian
    PROCEEDINGS OF THE 26TH ACM INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS, FTFJP 2024, 2024, : 17 - 22
  • [44] Path Executions of Java']Java Bytecode Programs
    Soomro, Safeeullah
    Alansari, Zainab
    Belgaum, Mohammad Riyaz
    PROGRESS IN ADVANCED COMPUTING AND INTELLIGENT ENGINEERING, VOL 2, 2018, 564 : 261 - 271
  • [45] Java Bytecode Verification
    Tobias Nipkow
    Journal of Automated Reasoning, 2003, 30 : 233 - 233
  • [46] Extending operational semantics of the Java']Java bytecode
    Czarnik, Patryk
    Schubert, Aleksy
    TRUSTWORTHY GLOBAL COMPUTING, 2008, 4912 : 57 - 72
  • [47] Data-flow based vulnerability analysis and Java']Java bytecode
    Chen, Hua
    Zou, Tao
    Wang, Dongxia
    PROCEEDINGS OF THE 7TH WSEAS INTERNATIONAL CONFERENCE ON APPLIED COMPUTER SCIENCE: COMPUTER SCIENCE CHALLENGES, 2007, : 201 - +
  • [48] A Java']Java bytecode optimizer using side-effect analysis
    Clausen, LR
    CONCURRENCY-PRACTICE AND EXPERIENCE, 1997, 9 (11): : 1031 - 1045
  • [49] Java']Java bytecode verification for @NonNull types
    Male, Chris
    Pearce, David J.
    Potanin, Alex
    Dymnikov, Constantine
    COMPILER CONSTRUCTION, 2008, 4959 : 229 - 244
  • [50] Bytecode verification on Java']Java smart cards
    Leroy, X
    SOFTWARE-PRACTICE & EXPERIENCE, 2002, 32 (04): : 319 - 340
12345