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




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.

This paper will be presented at VMCAI'2023, colocated with POPL'2023 at Boston!

This paper will be presented at VMCAI'2023, colocated with POPL'2023 at Boston!

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 developed the prototype of the Tezos proof-of-stake blockchain.
  • 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.