Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23

Authors: Nicolas Berthier

Date: 2023-01-12

Category: Formal Methods

Tags: Java, security, tooling, static analysis, formal methods, formal verification, Development Tools

We are excited to announce that Nicolas will present a paper at the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) the 16th and 17th of January.

This year, VMCAI is co-located with the Symposium on Principles of Programming Languages (POPL) conference, which, as its name suggests, is a flagship conference in the Programming Languages domain.

What's more, for its 50th anniversary edition, POPL will return back where its first edition took place: Boston! It is thus in the vicinity of the MIT and Harvard that we will meet with prominent figures of computer science research.

A sound technique to statically guarantee security properties on Java bytecode

Nicolas will be presenting a novel static program analysis technique dedicated to the discovery of information flows in Java bytecode. By automatically discovering such flows, the new technique allows developers and users of Java libraries to assess key security properties on the software they run.

Two prominent examples of such properties are confidentiality (stating that no single bit of secret information may be inadvertently revealed by the software), and its dual, integrity (stating that no single bit of trusted information may be tampered via untrusted data).

The technique is proven sound (i.e. it cannot miss a flow of information), and achieves state-of-the-art precision (i.e. it does not raise too many false alarms) according to evaluations using the IFSpec benchmark suite.

Try it out!

In addition to being supported by a proof, the technique has also been implemented in a tool called Guardies.

We believe this static analysis tool will naturally complement the taint tracking and dynamic analysis techniques that are usually employed to assess software security.

Reading more about it

You may already access the full paper here.

Nicolas developed this contribution while working at the University of Liverpool, in collaboration with Narges Khakpour, herself from the University of Newcastle.

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

• We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, Wasm and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
• We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we helped the French Income Tax Administration re-adapt and improve their internally kept M language, we designed a DSL to model and express revenue streams in the Cinema Industry, codename Niagara, and we also developed the prototype of the Tezos proof-of-stake blockchain from 2014 to 2018.
• We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
• We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.