-
Sawja: Static Analysis Workshop for Java
Authors:
Laurent Hubert,
Nicolas Barré,
Frédéric Besson,
Delphine Demange,
Thomas Jensen,
Vincent Monfort,
David Pichardie,
Tiphaine Turpin
Abstract:
Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when develo** a full-fledged analyzer for a realistic language such as Java. This paper describes the Sawja library: a static analysis framework fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main feat…
▽ More
Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when develo** a full-fledged analyzer for a realistic language such as Java. This paper describes the Sawja library: a static analysis framework fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main features of the library, including (i) efficient functional data-structures for representing program with implicit sharing and lazy parsing, (ii) an intermediate stack-less representation, and (iii) fast computation and manipulation of complete programs.
△ Less
Submitted 20 July, 2010;
originally announced July 2010.
-
Verification of Java Bytecode using Analysis and Transformation of Logic Programs
Authors:
Elvira Albert,
Miguel Gómez-Zamalloa,
Laurent Hubert,
German Puebla
Abstract:
State of the art analyzers in the Logic Programming (LP) paradigm are nowadays mature and sophisticated. They allow inferring a wide variety of global properties including termination, bounds on resource consumption, etc. The aim of this work is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode (JVML). In order to achieve our goal,…
▽ More
State of the art analyzers in the Logic Programming (LP) paradigm are nowadays mature and sophisticated. They allow inferring a wide variety of global properties including termination, bounds on resource consumption, etc. The aim of this work is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode (JVML). In order to achieve our goal, we rely on well-known techniques for meta-programming and program specialization. More precisely, we propose to partially evaluate a JVML interpreter implemented in LP together with (an LP representation of) a JVML program and then analyze the residual program. Interestingly, at least for the examples we have studied, our approach produces very simple LP representations of the original JVML programs. This can be seen as a decompilation from JVML to high-level LP source. By reasoning about such residual programs, we can automatically prove in the CiaoPP system some non-trivial properties of JVML programs such as termination, run-time error freeness and infer bounds on its resource consumption. We are not aware of any other system which is able to verify such advanced properties of Java bytecode.
△ Less
Submitted 19 July, 2010;
originally announced July 2010.
-
Soundly Handling Static Fields: Issues, Semantics and Analysis
Authors:
Laurent Hubert,
David Pichardie
Abstract:
Although in most cases class initialization works as expected, some static fields may be read before being initialized, despite being initialized in their corresponding class initializer. We propose an analysis which compute, for each program point, the set of static fields that must have been initialized and discuss its soundness. We show that such an analysis can be directly applied to identify…
▽ More
Although in most cases class initialization works as expected, some static fields may be read before being initialized, despite being initialized in their corresponding class initializer. We propose an analysis which compute, for each program point, the set of static fields that must have been initialized and discuss its soundness. We show that such an analysis can be directly applied to identify the static fields that may be read before being initialized and to improve the precision while preserving the soundness of a null-pointer analysis.
△ Less
Submitted 20 July, 2010; v1 submitted 19 July, 2010;
originally announced July 2010.
-
A Non-Null Annotation Inferencer for Java Bytecode
Authors:
Laurent Hubert
Abstract:
We present a non-null annotations inferencer for the Java bytecode language. We previously proposed an analysis to infer non-null annotations and proved it soundness and completeness with respect to a state of the art type system. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on…
▽ More
We present a non-null annotations inferencer for the Java bytecode language. We previously proposed an analysis to infer non-null annotations and proved it soundness and completeness with respect to a state of the art type system. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.
△ Less
Submitted 19 July, 2010;
originally announced July 2010.
-
Enforcing Secure Object Initialization in Java
Authors:
Laurent Hubert,
Thomas Jensen,
Vincent Monfort,
David Pichardie
Abstract:
Sun and the CERT recommend for secure Java development to not allow partially initialized objects to be accessed. The CERT considers the severity of the risks taken by not following this recommendation as high. The solution currently used to enforce object initialization is to implement a coding pattern proposed by Sun, which is not formally checked. We propose a modular type system to formally sp…
▽ More
Sun and the CERT recommend for secure Java development to not allow partially initialized objects to be accessed. The CERT considers the severity of the risks taken by not following this recommendation as high. The solution currently used to enforce object initialization is to implement a coding pattern proposed by Sun, which is not formally checked. We propose a modular type system to formally specify the initialization policy of libraries or programs and a type checker to statically check at load time that all loaded classes respect the policy. This allows to prove the absence of bugs which have allowed some famous privilege escalations in Java. Our experimental results show that our safe default policy allows to prove 91% of classes of java.lang, java.security and javax.security safe without any annotation and by adding 57 simple annotations we proved all classes but four safe. The type system and its soundness theorem have been formalized and machine checked using Coq.
△ Less
Submitted 19 July, 2010;
originally announced July 2010.
-
Magnon-polaron and Spin-polaron Signatures in the Specific Heat and Electrical Resistivity of $La_{0.6}Y_{0.1}Ca_{0.3}MnO_3$ in Zero Magnetic Field, and the Effect of $Mn-O-Mn$ Bond Environment
Authors:
M. Ausloos,
L. Hubert,
S. Dorbolo,
A. Gilabert,
R. Cloots
Abstract:
$La_{0.6}Y_{0.1}Ca_{0.3}MnO_{3}$, an $ABO_{3}$ perovskite manganite oxide, exhibits a non trivial behavior in the vicinity of the sharp peak found in the resistivity $ρ$ as a function of temperature $T$ in zero magnetic field. The various features seen on $dρ/dT$ are discussed in terms of competing phase transitions. They are related to the $Mn-O-Mn$ bond environment depending on the content of…
▽ More
$La_{0.6}Y_{0.1}Ca_{0.3}MnO_{3}$, an $ABO_{3}$ perovskite manganite oxide, exhibits a non trivial behavior in the vicinity of the sharp peak found in the resistivity $ρ$ as a function of temperature $T$ in zero magnetic field. The various features seen on $dρ/dT$ are discussed in terms of competing phase transitions. They are related to the $Mn-O-Mn$ bond environment depending on the content of the $A$ crystallographic site. A Ginzburg-Landau type theory is presented for incorporating concurrent phase transitions. The specific heat $C$ of such a compound is also examined from 50 till 200 K. A log-log analysis indicates different regimes. In the low temperature conducting ferromagnetic phase, a collective magnon signature ($C \simeq T^{3/2}$) is found as for what are called magnon-polaron excitations. A $C \simeq T^{2/3}$ law is found at high temperature and discussed in terms of the fractal dimension of the conducting network of the weakly conducting (so-called insulating) phase and Orbach estimate of the excitation spectral behaviors. The need of considering both independent spin scattering and collective spin scattering is thus emphasized. The report indicates a remarkable agreement for the Fisher-Langer formula, i.e. $C$ $\sim$ $dρ/dT$ at second order phase transitions. Within the Attfield model, we find an inverse square root relationship between the critical temperature(s) and the total local $Mn-O-Mn$ strain.
△ Less
Submitted 14 September, 2002;
originally announced September 2002.