-
Bridging the Gap between Technical Heterogeneity of Context-Aware Platforms: Experimenting a Service Based Connectivity between Adaptable Android, WComp and OpenORB
Authors:
Valerie Monfort,
Sihem Cherif
Abstract:
Many companies include in their Information Systems (IS) several communicating heterogeneous middleware according to their technical needs. The need is the same when IS requires using context aware platforms for different aims. Moreover, users may be mobile and want to receive and send services with their PDA that more often supports Android based Human Man Interface. In this paper, we show how we…
▽ More
Many companies include in their Information Systems (IS) several communicating heterogeneous middleware according to their technical needs. The need is the same when IS requires using context aware platforms for different aims. Moreover, users may be mobile and want to receive and send services with their PDA that more often supports Android based Human Man Interface. In this paper, we show how we extend Android to make it adaptable and open. We also present how we communicate between different heterogeneous context aware platforms as WComp and OpenORB by using Android and Web Services. We introduce a concrete case study to explain our approach.
△ Less
Submitted 2 March, 2012;
originally announced March 2012.
-
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.
-
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.
