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

Auteurs: Nicolas Berthier

Date: 2023-01-12

Catégorie: 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.

Au sujet d'OCamlPro :

OCamlPro développe des applications à haute valeur ajoutée depuis plus de 10 ans, en utilisant les langages les plus avancés, tels que OCaml et Rust, visant aussi bien rapidité de développement que robustesse, et en ciblant les domaines les plus exigeants (méthodes formelles, cybersécurité, systèmes distribués/blockchain, conception de DSLs). Fort de plus de 20 ingénieurs R&D, avec une expertise unique sur les langages de programmation, aussi bien théorique (plus de 80% de nos ingénieurs ont une thèse en informatique) que pratique (participation active au développement de plusieurs compilateurs open-source, prototypage de la blockchain Tezos, etc.), diversifiée (OCaml, Rust, Cobol, Python, Scilab, C/C++, etc.) et appliquée à de multiples domaines. Nous dispensons également des [formations sur mesure certifiées Qualiopi sur OCaml, Rust, et les méthodes formelles] (https://training.ocamlpro.com/) Pour nous contacter : contact@ocamlpro.com.