2008 · 61 citations · 26 references
It is well known that the use of native methods in Java defeats Java’s guarantees of safety and security, which is why the default policy of Java applets, for example, does not allow loading non-local native code. However, there is already a large amount of trusted native C/C++ code that comprises a significant portion of the Java Development Kit (JDK). We have carried out an empirical security study on a portion of the native code in Sun’s JDK 1.6. By applying static analysis tools and manual inspection, we have identified in this security-critical code previously undiscovered bugs. Based on our study, we describe a taxonomy to classify bugs. Our taxonomy provides guidance to construction of automated and accurate bug-finding tools. We also suggest systematic remedies that can mediate the threats posed by the native code. 1
26
Extended static checking for Java
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge et al. · 2002 · 1.3K citations
Efficient software-based fault isolation
Robert Wahbe, Steven Lucco, Thomas E. Anderson et al. · 1993 · 1.2K citations · Full text
Software Maintenance, Engineering, Computer Architecture +19
James C. Corbett, Matthew B. Dwyer, John Hatcliff et al. · 2000 · 1.1K citations · Full text
Finite-state Verification Techniques, Engineering, Program Checking +15
Automatic predicate abstraction of C programs
Thomas Ball, Rupak Majumdar, Todd Millstein et al. · ACM SIGPLAN Notices · 2012 · 696 citations
Formal certification of a compiler back-end or
Xavier Leroy · 2006 · 648 citations · Full text