FM-BIASED - Formal Methods: Business Impact of Application to Security relevant Devices


Nowadays crucial system functions tend to be hardwired, such as protocols, parallel processing algorithms, operating system kernels, etc. This opens a prospect for application of formal methods to prove properties of relevant system components, like compliance to Common Criteria and more specialized standards such as NERC CIP (standards providing a cyber-security framework for the identification and protection of Critical Cyber Assets) and ISA 99. FM-BIASED is a study project on the establishment of the business impact of formal methods concerning compliance to the above standards in several industrial and business sectors where such regulations are enforced or will soon be enforced. In most of those sectors, compliance verification may be difficult because most automation are legacy systems, so that industrial stakeholders must face the prospect of either trying to validate ageing systems designed many years ago, or redesigning/re-implementing their functions anew.
  • Skills/Topics:

    • safety
    • security
    • formal methods
    • drones
Universitá del Piemonte Orientale (Coordinator Italy) Deloitte Advisory S.L. (Spain)
CNR-Ceris (Italy)
Katholieke Universiteit Leuven (Belgium).


Our Role
1. To survey the current state of the art of formal methods and tools, with a view to single out those methods whose industrial application appears most promising in selected business sectors. 2. Workshop with the industrial advisory panel to discuss several prospective case studies. One of the case studies is oriented to the sense & avoid control system of UAVs (Unmanned Air Vehicles). 3. Feasibility assessment and cost of formal methods application to prove security compliance in selected use case. 4. Impact analysis to estimate relevant benefits in the application areas due to formal proof of properties on the legal and insurance respect.