PhD position - Multi-level specification and verification of cybersecurity properties for critical C programs

OPPORTUNITY DETAILS

Total reward

0 $

State University

CEA Tech

Area

Western Europe

Host Country

France

Deadline

31 Oct 2021

Study level

Doctoral Degree

Opportunity type

PhD

Specialities

Information technology and computer science

Opportunity funding

Not funding

Eligible Countries

This opportunity is destined for all countries

Eligible Region

All Regions

SL-DRT-21-0866

RESEARCH FIELD

Cyber security : hardware and sofware

ABSTRACT

This topic deals with formal specification and verification of software properties, in particular cybersecurity properties. Deductive verification tools allow their users to mathematically prove that a given software implementation is correct with respect to a set of formally specified properties. This is notably the case with the WP plug-in of the Frama-C framework for C programs and ACSL specifications. Another plug-in, MetAcsl, was recently developed in order to ease expressing and verifying High-level properties, with a focus on cybersecurity-related properties (e.g. memory isolation, confidentiality, or integrity). Notably, MetAcsl allows users to pose constraints on all read or write accesses in the program.In practice, verifying such high level properties on complex industrial software is often hindered by a low success rate of the automated theorem provers over the proof obligations generated by deductive verification tools. This is due to two main reasons. First, such software tends to use low-level operations (e.g. bitwise operators or pointer casts), which are difficult to represent in the logic world, hence rendering the proof much more complex. Second, the sheer quantity and complexity of mostly independent properties, notably invariants of complex data structures, can prevent the automated provers from succeeding.However, it is often the case that each function only has an impact on a tiny part of the properties, leaving most of them untouched. As all the properties must a priori be considered in the proof context, the latter is thus needlessly cluttered. Moreover, in a certain number of cases, proving the preservation of the impacted property could be done much more easily at a more abstract level. In addition, higher-level properties are usually also more easily understandable, thereby easing the task of the validation team. Similarly, an abstract executable model can be animated and evaluated more easily than the real code.The aim of this PhD is to propose a multi-level specification and verification framework for C programs. This will include verifying a part of the properties on an abstract version of the software under analysis. The abstract version will take the form of a simpler C code (abstracting away parts of the concrete system), encoding for instance a transition system, while staying sufficiently representative to let users state their properties of interest. As is the case in existing refinement-based techniques (in particular the B method), the links between the abstract system and the real code will need to be rigorously established in order to ensure the correctness of the whole development. Hence the verification of the real code will be made easier, since it will be sufficient to show that it respects the refinement properties to be able to deduce that the high-level properties stated on the abstract system also hold for the real code.Specification and verification of the refinement properties can take advantage of the work done in the MetAcsl plug-in. For instance, MetAcsl already offers some functionalities for proving more easily that if a function does not modify the footprint of a property (i.e. the locations that are read by the property), then the property is preserved by the function.The first part of the PhD will be dedicated to the definition of a methodology for specifying an abstract representation of a concrete software implementation. In particular, a way to define the links between data structures and function of both systems, as well as their properties, will be defined. In addition, refinement properties assuring that if a property is proved on the abstract system, then its concrete counterpart holds as well will be formally stated, too.The proposed technique must be able to be deployed on complex industrial software (using optimized data structures, with low-level operations and many invariants that need to be preserved), in order to verify cyber-security properties. To ensure that, a bottom-up approach can be followed, starting from an existing concrete implementation and actual properties that need to be proved on this implementation. For instance one might want to prove on an abstract level that a resource handling mechanism (memory allocator, task manager in a micro kernel, ...) respects a given access policy. Again, MetAcsl could be used for proving the refinement properties towards the real code.A second step in the PhD will be dedicated to develop a tool for automating the abstractions and refinements. Again, the tool will be evaluated on concrete case studies, either open-source or done in the context of industrial projects.