How do we know that we can trust software? One answer is software reliability testing.
Dr Mário Pereira and Dr António Ravara from the Nova School of Science and Technology in Lisbon, Portugal, and their collaborators have developed the Cameleer tool, a formal verification software tool for OCaml-written code.
Read the original article: https://doi.org/10.1007/978-3-030-81688-9_31
Read more in Research Outreach
Image credit: RedPixel.PL/Shutterstock
Transcript:
Hello and welcome to Research Pod! Thank you for listening and joining us today.
In this episode, we will be looking at the research of Dr Mário Pereira from the Nova School of Science and Technology in Lisbon, Portugal. He and his collaborators developed the Cameleer tool, a formal verification software for OCaml-written code.
The world has become dependent on software. From its use in everyday tasks, such as social networks, to highly critical missions, such as space exploration, software is the mainstay that keeps our world operating. Software development is an error-prone activity, to say nothing of its susceptibility to malicious attacks. Defective software can have embarrassing and expensive consequences. For instance, in 2015, a failure occurred during a daily system refresh shut down in the point-of-sales systems of 7,000 Starbucks stores in the United States and 1,000 in Canada. Employees were unable to accept card payments or register change, so they were forced to give customers free coffee and tea. Although the problem was fixed a few hours later, Starbucks is reported to have lost between 3 and 4 million dollars that day. Another example occurred in 2008 when the new Heathrow Terminal 5 opened and with it the promise of a modern, efficient, and functioning baggage handle system. The system was tested prior to opening with over 12,000 pieces of luggage and worked perfectly. When the terminal opened to the public, the system was unable to cope with the vast amount of luggage checked in every day, and only ten days after its launch, approximately 42,000 bags were lost and more than 500 flights cancelled.
So how do we know that we can trust software? One answer is software reliability testing. Still, such tests only cover a subset of the possible executions that the software will run in practice. The best solution involves including robust mathematical guarantees in the software development process. ‘Formal methods’ is a field within computer science that advocates this approach, employing rigorous mathematical reasoning and modelling techniques to describe and certify parts of computer infrastructures and provide formal software verification. In line with this practice, Dr Mário Pereira and Dr António Ravara from the Nova School of Science and Technology in Lisbon, Portugal, and their collaborators have developed the Cameleer tool, a formal verification software tool for OCaml-written code.
Deductive software verification involves expressing the correctness of code into a set of mathematical statements, known as verification conditions, and then proving them. Pereira explains how this includes a logical specification that is attached to the code. A logical specification is a description, written in a mathematical language, of the properties that a program must respect at certain points of its execution. Finally, a verification conditions generator algorithm is implemented. This takes the code together with its specification and produces the verification conditions. Proving these mathematical statements formally establishes that the program execution obeys the logical properties described in its specification. Pereira remarks that despite the advances in deductive verification and proof automation in past decades, the family of functional languages, used to construct programs by applying and composing functions, has received little attention.
One such functional language is OCaml, an industrial-strength programming language developed at the Inria Paris Research Centre. OCaml is used to implement software such as proof assistants, automated solvers, and compilers in industry throughout the world by organisations including Facebook and Bloomberg. OCaml is a multi-paradigm language supporting functional, imperative, and object-oriented programming. It has a robust pattern-matching mechanism, a flexible module system, and automatic memory management, so it can be used to write efficient, modular programs that maintain type-safety, meaning preventing type errors caused by discrepancies between differing data types, and deals with side effects such as memory mutation.
Even though these factors make OCaml code a good fit for formal verification, deductive verification has rarely been used with OCaml programs. Prior to the Cameleer project, an automated verification tool that can deal directly with code written in OCaml didn’t even exist. Until now, OCaml programmers choosing to employ proof automation have had to learn a verification-aware language, write programs in it, and then perform code extraction. The alternative was to use tools that necessitated manual proof assistance.
A specification language is a formal language used during software development that enables precise specification at different levels. It is required to carry out formal software verification. A specification language specifies the semantics and structure of a software system and is used during formal verification to provide mathematical proof that a system works according to prior specifications.
Together with Dr Arthur Charguéraud, Dr Jean-Christophe Filliâtre and Dr Cláudio Belo Lourenço, Pereira has developed a specification language for OCaml, called GOSPEL – or Generic Ocaml SPEcification Language. Since then, GOSPEL has grown into a mature project, currently being developed by a large consortium of researchers which include Clément Pascutto, Nicolas Osborne, Dr François Pottier, and Dr Armaël Guéneau. GOSPEL is designed to facilitate the verification of data structures and algorithms. It has formal semantics that are defined by translating into Separation Logic, a form of reasoning about programs. GOSPEL offers a high-level, concise syntax that is accessible to programmers who are not familiar with Separation Logic. While GOSPEL was developed to specify OCaml code, it is also intended as a generic tool for verification and testing with features that could be applied to other programming languages.
The researchers have developed Cameleer, the first automated deductive software verification tool for programs written in OCaml. They selected GOSPEL as the specification language to allow them to assign readable, rigorous, behavioural specification to the OCaml code. Cameleer focuses on proof automation and takes a GOSPEL-annotated OCaml program as input. It translates this into WhyML. WhyML is the programming and specification language of Why3, a platform for deductive software verification, and in particular automated proof. Why3’s verification condition generator produces a set of verification conditions that are sent to different solvers where formal proofs are performed.
Pereira and his colleagues chose to develop the Cameleer verification tool to accept programs written directly in OCaml as input, rather than a dedicated proof language. This means that the user does not have to re-write their entire OCaml source code solely for the purpose of carrying out formal verification. Throughout the verification process, the user only has to write the OCaml code and the GOSPEL specification. Cameleer has been designed so that the other elements are automatically generated; subsequently, the user doesn’t have to be concerned with the program generated in WhyML. The user is only involved in the initial specifying phase and in the final step of the process where they help Why3 to close the proof.
To evaluate Cameleer’s performance and usability, the researchers compiled a test suite of case studies made up of over 1,000 lines of OCaml code. These included implementations from existing libraries such as numerical programs, sorting and searching, logical algorithms, array scanning, higher-order implementations, and several historical algorithms. These were all successfully verified using the Cameleer tool. Pereira adds that this collection of case studies alone contributes towards a comprehensive body of verified OCaml codebases.
Pereira describes how the researchers working on the Cameleer project continue to push the frontiers of software formal verification. They are developing principles and tools for the application of deductive verification to OCaml-written code. To date, they have produced a robust tool that can handle OCaml code and automatically verify that it adheres to a specification written in GOSPEL. Their work continues in their development of a powerful, usable and mostly automated verification framework for the OCaml community, making verification more accessible to programmers using OCaml – including those that are not verification experts. About the next steps in their research, Pereira says: ‘Our ultimate goal is to grow Cameleer to a verification tool that can simultaneously benefit from the best features of different intermediate verification frameworks.’
That’s all for this episode – thanks for listening, and stay subscribed to Research Pod for more of the latest science. See you again soon.
Leave a Reply