To minimize resource usage, energy consumption and exposure of services, system design in distribution grids, sensor networks, connected objects, employs methods to specialize a system library with the program that specifies its designated service on the target networked architecture or hypervisor: system programming.
The goal of our project is to explore, define and prototype, fundamental aspects toward the construction of safe and secure system programs in a possibly certified runtime environment:
• System stealth and security – services implemented using system programs boot fast and respond quickly (booting the service in parallel of the client's request). Minimized exposure paired with layered verification of inferred data and information flow properties of system programs make them ideal to device stealth and resilient network services.
• Architecture analysis and integration – Just as the AADL was initially designed to integrate ADA programs on embedded architecture, we seek the definition of a framework to structure the architecture system programs are integrated with, to define functional and non-functional characteristics relevant to that architecture, to check and optimize the allocation of the system program on the target architecture using contracts, interfaces.
• Type-based program analysis – we seek the use of value-dependent types subject to logical properties, e.g. liquid types or refinement types, to express functional properties (invariants about program values) as well as non-functional properties or effects, pertaining to the usage of resources (memory, system calls, communication, devices, hypervisor) to verify security policies, architecture integration, functional behavior.
Implementation of prototypes will be conducted using high-level programming languages such as Haskell or Ocaml. It will possibly reuse existing, open-source, implementations of refinement types, as well as powerful SAT/SMT solvers, such as Z3, to gain scalability.
A Master in Theoretical Computer Science with demonstrated experience in type theory, logic and verification, programming languages, operating systems, is a prerequisite for application. Good spoken and written scientific English will be beneficial, as well as demonstrated teamwork skills.