The Coq mailing list

[Jean-Pierre <jean-pierre.talpin AT inria.fr>]

Dear colleagues,

 I am forwarding you the following PhD proposal in the context of project 
RIOT-fp (future-proof operating systems for IoT) should you have a recent 
master student with background in theorem proving (Coq, Lean or Isabelle), 
interest in operating systems and in the Rust programming language.  Please 
feel free to distributed the attached ad around you, and apologies for 
multiple copies.
Best regards,
Jean-Pierre

_____________________________________________________
Title: Compositional verification of system program libraries in Rust

Keywords: theorem proving, programming languages, operating systems, formal 
verification, dependent types, theory of contracts

Project RIOT-fp [b] is an Inria Challenge with the objective of developing 
future-proof operating system libraries [1,3] for application to IoT: RIOT 
[a].  Our PhD project is interested in one of the futures of RIOT: RIOT-rs, 
implemented in Rust [c]. This computing base provides access to a vast 
ecosystem of analysis, code generation, verification and proof tools [d,e,f]. 
It offers us to rethink a system software validation process that would suit 
both system programming and verification requirements (as one may expect from 
using, e.g., a theorem prover).

The notion of contract [2] is one such interface between the development and 
verification of system programs.  A contract allows, on one hand, to formally 
document the hypothesis and guarantees of system modules, functions, 
artifacts, with respect to global safety ad security requirements.  Contracts 
can be sufficiently abstract and comprehensible for system programmers, and 
adequately refined to meet the strongest requirements of mechanized 
verification.

Our project will focus on the development of such a modular validation flow 
by case-studying the core of RIOT's implementation in Rust [riot-rs-core].  
We define and exercise this workflow to characterize and validate global 
requirements ranging from race-condition, deadlock avoidance, priority 
management and schedulability, and/or memory isolation, fault isolation, 
information flow control.

The project will be implemented with teams Tea and Celtique at Inria, Rennes, 
in close collaboration with RIOT-fp teams in Paris.  It requires a Master 
degree with solid background in proof theory and mathematical logic, 
programming languages and type theory, as well as motivation and interest in 
both the implementation and verification of operating systems.  Prior 
knowledge and experiences with Rust and either Coq, Iris and/or Lean, F* will 
stand out. 

Please visit  https://jobs.inria.fr/public/classic/en/offres/2022-04915 for 
detailed information and for application


BIBLIOGRAPHY
[a] RIOT: http://www.riot-os.org
[b] RIOT-fp: https://future-proof-iot.github.io/RIOT-fp
[c] riot-rs-core: 
https://github.com/future-proof-iot/RIOT-rs/tree/main/src/riot-rs-core/src

REFERENCES
[1] "Verified Functional Programming of an IoT operating system’s 
boot-loader". International Conference on Formal Methods and Models for 
System Design, 2021.
[2] "A Mechanically Verified Theory of Contracts". International Colloquium 
on Theoretical Aspects of Computing, 2021.
[3] "End-to-end Mechanized Proof of an eBPF Virtual Machine for 
Microcontrollers". International Conference on Computer Aided Verification, 
2022.