Pietro Ferrara
Agostino Cortesi
Fausto Spoto
ABSTRACT
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.
- Checkstyle. http://checkstyle.sourceforge.net. Accessed on March, 16th 2018.Google Scholar
- Clr to jvm. http://www.xmlvm.org/clr2jvm/. Accessed on March, 16th 2018.Google Scholar
- CodeSonar - Static Analysis SAST Software. https://www.grammatech.com/products/codesonar. Accessed on March, 16th 2018.Google Scholar
- Findbugs<sup>TM</sup> - Find Bugs in Java Programs. http://findbugs.sourceforge.net/. Accessed on March, 16th 2018.Google Scholar
- Ndepend. http://www.ndepend.com. Accessed on March, 16th 2018.Google Scholar
- .Net Reflector Add-Ins. https://www.microsoft.com/en-us/research/project/spec.Google Scholar
- PMD. https://pmd.github.io/. Accessed on March, 16th 2018.Google Scholar
- WALA. http://wala.sourceforge.net/wiki/index.php/Main_Page. Accessed on March, 16th 2018.Google Scholar
- M. Ameri and C. A. Furia. Why Just Boogie? Translating between Intermediate VÂćerification Languages. In Proceedings of IFM '16, LNCS. Springer, 2016. Google ScholarDigital Library
- R. Atkey and D. Sannella. ThreadSafe: Static Analysis for Java Concurrency. Electronic Comm. of the European Association of Software Science and Technology, 72, 2015.Google Scholar
- G. Barbon, A. Cortesi, P. Ferrara, and E. Steffinlongo. DAPA: degradation-aware privacy analysis of android apps. In Proceedings of STM '16, pages 32--46, 2016.Google ScholarCross Ref
- M. Barnett, K. Leino, and W. Schulte. The Spec# Programming System: An Overview. In Proceedings of CASSIS '04, 2004. Google ScholarDigital Library
- M. Bebenita, F. Brandner, M. Fähndrich, F. Logozzo, W. Schulte, N. Tillmann, and H. Venter. SPUR: a Trace-based JIT Compiler for CIL. In W. R. Cook, S. Clarke, and M. C. Rinard, editors, Proceedings of OOPSLA '10. ACM, 2010. Google ScholarDigital Library
- G. Costantini, P. Ferrara, and A. Cortesi. A suite of abstract domains for static analysis of string values. Softw., Pract. Exper., 45(2):245--287, 2015. 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 Proceedings of POPL '77. ACM Press, 1977. 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 Proc. of Principles of Programming Languages (POPL'77), pages 238--252, 1977. Google ScholarDigital Library
- Coverity. Coverity Prevent<sup>TM</sup> . http://www.coverity.com/library/pdf/coverity_prevent.pdf. Accessed on March, 16th 2018.Google Scholar
- ECMA. Standard ECMA-335: Common Language Infrastructure (CLI). 2012.Google Scholar
- T. A. S. Foundation. Apache Commons BCEL. https://commons.apache.org/proper/commons-bcel. Accessed on March, 16th 2018.Google Scholar
- JetBrains. Resharper. https://www.jetbrains.com/resharper.Google Scholar
- T. Lindholm, F. Yellin, G. Bracha, and A. Buckley. The Java Virtual Machine Specification, Java SE 7 Edition. Addison-Wesley Professional, 1st edition, 2013. Google ScholarDigital Library
- F. Logozzo. Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes. In Proceedings of VMCAI '07, LNCS. Springer, 2007. Google ScholarDigital Library
- F. Logozzo and M. Fähndrich. Static Contract Checking with Abstract Interpretation. In Proceedings of FoVeOOS '10, LNCS. Springer, 2010.Google Scholar
- Microsoft. FxCop. https://msdn.microsoft.com/en-us/library/bb429476(v=vs.80).aspx. Accessed on March, 16th 2018.Google Scholar
- F. Spoto. The Julia Static Analyzer for Java. In Proceedings of SAS '16, LNCS. Springer, 2016.Google ScholarCross Ref
- Wikipedia. List of Tools for Static Code Analysis. https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis#Java. Accessed on March, 16th 2018.Google Scholar
Recommendations
From CIL to Java bytecode: Semantics-based translation for static analysis leveraging
Highlights- A formal translation of CIL (.Net) bytecode into Java bytecode is introduced and proved sound w.r.t. the language semantics
AbstractA 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. ...
Decompiling Java Bytecode: Problems, Traps and Pitfalls
CC '02: Proceedings of the 11th International Conference on Compiler ConstructionJava virtual machines execute Java bytecode instructions. Since this bytecode is a higher level representation than traditional object code, it is possible to decompile it back to Java source. Many such decompilers have been developed and the ...
Java bytecode to native code translation: the caffeine prototype and preliminary results
MICRO 29: Proceedings of the 29th annual ACM/IEEE international symposium on MicroarchitectureThe Java bytecode language is emerging as a software distribution standard. With major vendors committed to porting the Java run-time environment to their platforms, programs in Java bytecode are expected to run without modification on multiple ...
Comments