Decrease size
Reset to Default
Increase size

FMSAFE: A Networked Centre for Formal Methods in Validation and Certification Procedures for Safety Critical ICT Systems

Primary Information

Domain

Information & Communication Technology

Project No.

5496

Sanction and Project Initiation

Sanction No: F. No.: 3-18/2015-TS-TS.I

Sanction Date: 29/11/2016

Project Initiation date: 08/02/2017

Project Duration: 36

Partner Ministry/Agency/Industry

Ministry of Human Resource Development, Ministry of Railways

 

Role of partner:The initial goal defined for the partner organization was to provide funding and give directions w.r.t. identifying the relevant research problems in the area of applying formal methods for Railway Systems validation.

 

Support from partner:None received so far

Principal Investigator

PI Image

PALLAB DASGUPTA
INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR

Host Institute

Co-PIs

PI Image

SANDEEP SHUKLA
INDIAN INSTITUTE OF TECHNOLOGY KANPUR

PI Image

SUPRATIK CHAKRABORTY
INDIAN INSTITUTE OF TECHNOLOGY BOMBAY

PI Image

P P CHAKRABARTI
INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR

PI Image

INDRANIL SAHA
INDIAN INSTITUTE OF TECHNOLOGY KANPUR

PI Image

SOUMYAJIT DEY
INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR

PI Image

ARITRA HAZRA
INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR

 

Scope and Objectives

Our aim is to grow a national knowledge centre for formal methods, targeting recent applications and safety standards in various ICT domains such as aeronautics, automotive, power, nuclear, railway, and space. Objectives include research and development of specific tools and tool repositories, industrial partnership and manpower training. We propose research centric work packages for developing tools for formal validation of control systems, networked systems, and hardware/software systems. We propose knowledge centric work packages on interpretation of safety standards, processes, and tool flows. We propose training centric work packages for developing the ecosystem for safety validation and certification procedures.

Deliverables

Final deliverables include novel tools for the problems outlined under the research centric work packages. Specifically:WP -R-1 (Deliverable from IIT Kharagpur): Tool for modelling and validation of hybrid dynamical systems consisting of software, platform and plant, using satisfiability modulo theory. WP-R-2 (Deliverable from IIT Bombay): Parallelized tools and techniques for checking formal properties of large software and hardware systems. WP-R-3 (Deliverable from IIT Kanpur): Formal tools and methodologies for verifying implementations of parts of TCP/IP protocol stack, as well as security protocol libraries such as OpenSSL, OpenSSH including TLS Library. Reverse engineering methodologies and tools proven on application layer protocols used in SCADA systems.Outcomes from the knowledge centric packages, WP-K-1 and WP-K-2, includes reports interpreting the formal verification mandate in industrial safety standards targeting specific application domains (of interest to our partners in avionics, automotive and railways), and prescribed tool flows for carrying out the recommendations.

 

Project image
Project image

Videos

 

Scientific Output

IITKGP: We have built a prototype tool framework, which takes plant dynamics and controller software as inputs. Our tool framework encodes the closed-loop execution of the plant and the controller into SMT clauses and verifies stability and other control performance properties. We have come up with a first-cut implementation of the tool. This first cut implementation helps us in identifying scalability issues with Hybrid SMT formulations. Initial results for various case studies have been reported. We have resolved certain scalability issues partially, i.e., pruning of the state-space by suitable compiler methods have been implemented. We are now working on algorithm development for adaptive step-size selection that facilitates scalable SMT techniques for Nonlinear systems. IITK: Security vulnerability study of SCADA protocols and discovery of threats in existing protocols, Formal modelling of SSL/TLS, OpenSSL vulnerability study. Methodology for translation of a nonlinear Simulink/Stateflow model to Linear Hybrid Automata (LHA) has been developed and applied to three benchmark examples manually. We are working on automating the translation process, identifying interesting properties for the example systems and verifying the generated LHA against those properties. IITB: We have already built two prototype implementations for automatic disjunctive decompositions, one of which exploits parallel computational resources, while the other exploits structure in the representation of the transition relation. These also serve as Boolean functional synthesis tools, and are among the best performing tools available today. We are also in an advanced stage of development of the ALaRE framework for specifying hybrid reachability algorithms. Finally, we have implemented some new abstract domains for our static assertion checker, and have implemented a prototype algorithm for refining the abstraction in one domain using information from another domain, without using the expensive reduced product operation. Our static analysis tool, CAnalyzer/C-SAFE, is being augmented with these new capabilities.

 

Project image
Project image

Results and outcome till date

IITKGP: Scalable Algorithms for Hybrid Control System Verification and validation. IITB: Automatic decomposition algorithms (parallel and sequential) for disjunctive decomposition of sequential circuits, ALaRE framework for on-the-fly interleaving of reachability algorithms, C-SAFE tools for assertion checking using plug-compile-play abstract domains. IITK: Methodology for translation of a Simulink/Stateflow model to Linear Hybrid Automata

 

Societal benefit and impact anticipated

Formal methods are techniques based on computational logic, automata theory and language semantics for proving the correctness of various safety-critical ICT systems such as integrated circuits, embedded software, railway signaling logic, control systems, network and security protocols etc. The use of formal methods have been recommended in several international industrial safety standards, including aeronautics (DO-178C), automotive (ISO 26262), industrial process automation (IEC 61508), nuclear (IEC 60880), power substation automation (IEC 61850), railway (EN 50128), space (ECSS-Q-ST-80C) and IEEE1228-1994 (software systems). Industry is facing a serious challenge in interpreting these recommendations in the Indian context and creating suitable tool flows. Cyber-security is another safety aspect where the Indian critical industries are weak and dependent on foreign products. FMSAFE is groomed to be a national centre on formal methods which has the following mandates. 1) create customized tool chains for various ICT domains, 2) perform fundamental research on the core formal techniques, and 3) serve the primary training and manpower requirements for industry, research establishments, and certification agencies. The partners of the project have already been successful in helping out organizations like HAL with the verification and validation requirements, for example we had been instrumental in formally verifying the first indigenous RTOS developed by HAL for airborne platforms. We also have important collaborations with Intel, Texas Instruments, Synopsys.

Next steps

IITKGP: 1. By mid- 2019 : we provide the first version of a tool for scalable SMT based analysis of complex nonlinear hybrid dynamics 2. By mid- 2020 : we validate the tool flow on large scale examples provided by industrial partners IITB: By mid-2019: (a) Developing techniques for automatically combining multiple abstract domains using SMT solving, for improving the precision of abstraction based software assertion checking. (b) Integrating improved automatic disjunctive decomposition along with existing techniques in parallel model checker. By end 2019: Implementing ALaRE based hybrid reachability algorithms and evaluating them. Developing automatic refinement techniques for multiple cooperating abstract domains (software assertion checking project) By mid 2020: Validating parallel model checker, hybrid reachability algorithms and static assertion checking tool on extensive benchmarks and real-life examples (if available). IITK: (i) Development of SCADA protocol security vulnerability detection methods. Currently penetration testing based discovery of threat models and vulnerabilities in progress with some successful attacks demonstrated. Formal modeling required. Expected Completion Oct 2019. (ii) Development of quantitative regular expression based network intrusion detection policies. Not started yet. Expected Completion Oct 2020. (iii) Model Based Development of Autopilot Software for Unmanned Vehicles. Modeling will be carried out in Simulink (end-2018) and and the model will be automatically translated to nonlinear hybrid systems model (mid-2019). For the verification of the nonlinear hybrid systems model, the verification technologies developed by the researchers at IITKGP will be employed (mid-2020). The counterexample produced by the verification tool will be used to automatically debug the Simulink model (mid-2020).

Publications and reports

IITKGP:
1. Rajorshee Raha, Pallab Dasgupta, Soumyajit Dey, "Algorithmic approaches for optimizing ECU time using multi-rate sampling", Control Theory and Technology (Springer), (accepted)
2. Sumana Ghosh, Soumyajit Dey and Pallab Dasgupta, "Co-synthesis of Loop Execution Patterns for Multi-Hop Control Networks", IEEE Embedded Systems Letters, (accepted)
3. Sumana Ghosh, Souradeep Dutta, Soumyajit Dey and Pallab Dasgupta, "A Structured Methodology for Pattern based Adaptive Scheduling in Embedded Control", ACM Transactions on Embedded Computing Systems (TECS), Volume 16, Issue 5s, September 2017, Article No. 189, Special Issue on ESWEEK 2017
4. A. A. B. da Costa, G. Frehse and P. Dasgupta, "Formal Feature Interpretation of Hybrid Systems," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. DOI: 10.1109/TCAD.2018.2857361 (accepted for presentation in EMSOFT 2018)
5. A. A. B. da Costa, P. Dasgupta (2017) ForFET: A Formal Feature Evaluation Tool for Hybrid Systems. In: D'Souza D., Narayan Kumar K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science, vol 10482. Springer, Cham
6. A. A. B. da Costa, S. Dharade, S. Mandal and P. Dasgupta, "AMS-Miner: Mining AMS Assertions Using Interval Arithmetic," 2018 31st International Conference on VLSI Design and 2018 17th International Conference on Embedded Systems (VLSID), Pune, 2018, pp. 404-409.
7. Sumana Ghosh, Dey Soumyajit and Pallab Dasgupta,"Synthesizing Performance-aware (m,k)-firm Control Execution Patterns under Dropped Samples", VLSI Design 2019

IITB:IITKGP:
1. Rajorshee Raha, Pallab Dasgupta, Soumyajit Dey, "Algorithmic approaches for optimizing ECU time using multi-rate sampling", Control Theory and Technology (Springer), (accepted)
2. Sumana Ghosh, Soumyajit Dey and Pallab Dasgupta, "Co-synthesis of Loop Execution Patterns for Multi-Hop Control Networks", IEEE Embedded Systems Letters, (accepted)
3. Sumana Ghosh, Souradeep Dutta, Soumyajit Dey and Pallab Dasgupta, "A Structured Methodology for Pattern based Adaptive Scheduling in Embedded Control", ACM Transactions on Embedded Computing Systems (TECS), Volume 16, Issue 5s, September 2017, Article No. 189, Special Issue on ESWEEK 2017
4. A. A. B. da Costa, G. Frehse and P. Dasgupta, "Formal Feature Interpretation of Hybrid Systems," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. DOI: 10.1109/TCAD.2018.2857361 (accepted for presentation in EMSOFT 2018)
5. A. A. B. da Costa, P. Dasgupta (2017) ForFET: A Formal Feature Evaluation Tool for Hybrid Systems. In: D'Souza D., Narayan Kumar K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science, vol 10482. Springer, Cham
6. A. A. B. da Costa, S. Dharade, S. Mandal and P. Dasgupta, "AMS-Miner: Mining AMS Assertions Using Interval Arithmetic," 2018 31st International Conference on VLSI Design and 2018 17th International Conference on Embedded Systems (VLSID), Pune, 2018, pp. 404-409.
7. Sumana Ghosh, Dey Soumyajit and Pallab Dasgupta,"Synthesizing Performance-aware (m,k)-firm Control Execution Patterns under Dropped Samples", VLSI Design 2019

IITB:
1. S. Chakraborty, D. Fried, L.M. Tabajara and M.Y. Vardi, "Functional Synthesis via Input-Output Separation", in Proc. of International Conference on Formal Methods in Computer-Aided Design (FMCAD), Oct 2018
2. S.Akshay, S. Chakraborty, S. Goel, S. Kulal and S. Shah, "What is Hard about Boolean Functional Synthesis", in Proc. of International Conference on Computer-Aided Verification (CAV), pg 251-269, Jul 2017 2. S. Chakraborty, A. Gupta and D. Unadkat, "Verifying Array Manipulating Programs by Tiling", in Proc. of Static Analysis Symposium (SAS), pg 428-449, Sep 2017
3. S. Akshay, S. Chakraborty, A. John and S. Shah, "Towards Parallel Boolean Functional Synthesis", in Proc. of International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pg 337-353, April 2017
4. S. Chakraborty, A. Gupta and R. Jain, "Matching Multiplications in Bit-vector Formulas", in Proc. of International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), pg. 131-150, Jan 2017

IITK:
1. Debleena Das, Ansuman Banerjee, Sandeep K. Shukla; "An automata theoretic framework for detecting schedulability attacks on cyber-physical systems", EAIT 2018 : Fifth International Conference on Emerging Applications of Information Technology, January 2018, Kolkata
2. Shubham Sharma, Rahul Gupta, Shubham Sahai Srivastava and Sandeep K. Shukla; "Detecting Insider Attacks on Databases using Blockchains", ACMSIGSAC Conference on Computer and Communications Security
3. S.Venkatesan, Shubham Sahai Srivastava and Sandeep Kumar Shukla; "Decentralized Authentication of IoT devices using Blockchain", 2nd Advanced Workshop on Blockchain: Technology, Applications, Challenges; IIT Bombay
4. Prachi Joshi, S. S. Ravi, Soheil Samii, Unmesh Bordoloi, Sandeep Shukla, Haibo Zeng; "Offset Assignment to Signals for Improving Frame Packing in CAN-FD", (accepted for) IEEE Real-Time Systems Symposium (RTSS 2017). Paris, France, December 2017
5. Tanmoy Kundu, Indranil Saha: Charging Station Placement for Indoor Robotic Applications. ICRA 2018: 3029-3036.
6. Sankar Narayan Das, Indranil Saha: Rhocop: receding horizon multi-robot coverage.

ICCPS 2018: 174-185.

1. S. Chakraborty, D. Fried, L.M. Tabajara and M.Y. Vardi, "Functional Synthesis via Input-Output Separation", in Proc. of International Conference on Formal Methods in Computer-Aided Design (FMCAD), Oct 2018
2. S.Akshay, S. Chakraborty, S. Goel, S. Kulal and S. Shah, "What is Hard about Boolean Functional Synthesis", in Proc. of International Conference on Computer-Aided Verification (CAV), pg 251-269, Jul 2017
2. S. Chakraborty, A. Gupta and D. Unadkat, "Verifying Array Manipulating Programs by Tiling", in Proc. of Static Analysis Symposium (SAS), pg 428-449, Sep 2017
3. S. Akshay, S. Chakraborty, A. John and S. Shah, "Towards Parallel Boolean Functional Synthesis", in Proc. of International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pg 337-353, April 2017
4. S. Chakraborty, A. Gupta and R. Jain, "Matching Multiplications in Bit-vector Formulas", in Proc. of International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), pg. 131-150, Jan 2017

IITK:
1. Debleena Das, Ansuman Banerjee, Sandeep K. Shukla; "An automata theoretic framework for detecting schedulability attacks on cyber-physical systems", EAIT 2018 : Fifth International Conference on Emerging Applications of Information Technology, January 2018, Kolkata
2. Shubham Sharma, Rahul Gupta, Shubham Sahai Srivastava and Sandeep K. Shukla; "Detecting Insider Attacks on Databases using Blockchains", ACMSIGSAC Conference on Computer and Communications Security
3. S.Venkatesan, Shubham Sahai Srivastava and Sandeep Kumar Shukla; "Decentralized Authentication of IoT devices using Blockchain", 2nd Advanced Workshop on Blockchain: Technology, Applications, Challenges; IIT Bombay
4. Prachi Joshi, S. S. Ravi, Soheil Samii, Unmesh Bordoloi, Sandeep Shukla, Haibo Zeng; "Offset Assignment to Signals for Improving Frame Packing in CAN-FD", (accepted for) IEEE Real-Time Systems Symposium (RTSS 2017). Paris, France, December 2017
5. Tanmoy Kundu, Indranil Saha: Charging Station Placement for Indoor Robotic Applications. ICRA 2018: 3029-3036. 6. Sankar Narayan Das, Indranil Saha: Rhocop: receding horizon multi-robot coverage. ICCPS 2018: 174-185.

Patents

None

Scholars and Project Staff

IITKGP
i. Mr. Jay Thakar, PhD (partially funded)
ii. Mr. Antonio Brutota Da Costa, PhD (partially funded)
iii. Mr. Surajit Roy, (admin asst)
iv. Mr. Sunandan Adhikary, MS
v. Ms. Sumana Ghosh, PhD (Partially funded)

IITB
i Mr. Ajeesh Kumar K., MTech RA (3 years)
ii. Ms. Mugdha U. Khedker (Jr. Res. Assistant -- resigned in Jul 2018 to join graduate studies, after working with us for 9 months)
iii. Mr. Chandrakant Talekar (part-time admin asst)
iv Dr. Hrishikesh Karmarkar (senior research scientist)
v Dr. Shetal Shah (senior research scientist)

IITK:
i. Ms. Debleena Das (Research Engineer, September, 2017 - January 2018)
ii. Mr. Nikhil Kumar Singh, (MS RA, January 2018 - till date)
iii. Mr. Shibashis Ghosh (Research Engineer, May 2018 - till date)
iv. Dr. Sankar Narayan Das (Postdoctoral Researcher, August 2018 - till date)

Challenges faced

In the original work plan, there were three types of work packages, namely Research centric, Knowledge centric and Training centric work packages. The later two were concerned with connecting with stakeholders and holding annual outreach workshops. Since no funds have been received so far from the Ministry of Railways, we have put on hold the knowledge and training centric work packages.

Other information

Committed Salary until March 2018 IITKGP: 3,80,000 IITB: 9,72,644 IITK: 4,00,000

Financial Information

  • Total sanction: Rs. 34710000

  • Amount received: Rs. 12500000

  • Amount utilised for Equipment: Rs. 2328986

  • Amount utilised for Manpower: Rs. 4593046

  • Amount utilised for Consumables: Rs. 15221

  • Amount utilised for Contingency: Rs. 213275.5

  • Amount utilised for Travel: Rs. 294205

  • Amount utilised for Other Expenses: 440

  • Amount utilised for Overheads: Rs. 2373150

Equipment and facilities

 

IITKGP: Server, Desktop, External HDD IITK: License for Mathworks Toolboxes IITB: Laptops (None required so far)