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 a multi institute project under IMPRINT (link), a MHRD supported Pan-IIT + IISc joint initiative for addressing major science and engineering challenges that are relevant in the national context. FMSAFE is groomed to be a national centre on formal methods which has the following mandates.
- create customized tool chains for various ICT domains,
- perform fundamental research on the core formal techniques, and
- serve the primary training and manpower requirements for industry, research establishments, and certification agencies.
Announcement
Activities: IIT Kharagpur
Development of a SMT based tool for modelling and validation of hybrid dynamical systems consisting of software, platform and plant.
Bounded model checking tools with back-end SAT/SMT solvers are being widely used today for the verification of discrete systems, such as programs and digital circuits. Systems having continuous dynamics (typically expressed using differential equations and hybrid automata) are treated in a very different way using techniques such as polyhedral approximation and generating functions. Software controlled embedded systems, which are widely used in safety critical domains, are essentially discretely controlled systems where the controller samples the plant at periodic intervals of time and determines the control actuation values. Today there is no tool for formal analysis of a software controlled continuous/hybrid plant, though tools for formally verifying the software in isolation exist. Formal verification and certification of embedded control systems will require a tool flow that can reduce the combination of an embedded software, its periodic pattern of execution, and the continuous/hybrid model of the plant into a common formalism and then prove end-to-end control requirements (safety, stability, robustness, control performance, etc.) on the unified specification. We propose to develop such a platform based on reduction of these artefacts into Satisfiability Modulo Theories (SMT).
Activities: IIT Bombay
Development of parallelizable techniques for checking properties of large software and hardware systems.
This work package aims to increase the scale of systems for which safety properties can be formally verified by leveraging the power of multiple processors/cores. Formal verification is known to be a computationally demanding task, and time-outs and memory-outs are not uncommon when verifying large and complex systems. By developing techniques that automatically decompose a verification task into sub-tasks that need only occasional synchronization/communication, and by delegating these sub-tasks to different processors/cores in a cluster of computers, we propose to address the scalability hurdle in formally verifying safety properties of large systems. In problem instances where exact verification cannot be achieved even with parallelization within available computing resources, the algorithms are intended to provide usable partial results, like coverage metrics, or a measure of confidence of the safety-correctness of the system. The technical work will leverage state-of-the-art technologies for (parallel) model checking, machine learning and constraint solving, and also involve developing new tools and techniques that give the user control over the precision-scalability tradeoff continuum.
Activities: IIT Kanpur
Development of provably correct and secure network artefacts
In this work package, our goals are (i) Development of formal tools and techniques for protocol reverse engineering to build models from implementation and verify their safety and security specifications; and (ii) Development of formal tools and methodologies to verify implementations of TCP/IP protocol stack, as well as security protocol libraries such as OpenSSL, OpenSSH including TLS Library.
Many protocol specifications are unknown, unavailable, or minimally documented, which prevents thorough analysis of the protocol for security purposes. For example, modern botnets often use undocumented and unique application layer communication protocols to maintain command and control over numerous distributed hosts. Inferring the specification of closed protocols has numerous advantages, such as intelligent Deep Packet Inspection, enhanced Intrusion Detection, and integration with legacy software packages. The multitude of closed protocols coupled with existing timeintensive reverse engineering methodologies for these protocols has spawned investigation into automated approaches for reverse engineering of closed protocols. If the protocols can be reverse engineered efficiently, one can verify safety of protocols, and also use the knowledge in thwarting cyber-attacks. A complementary strand of our research will consider the various application layer protocols, classify them according to their resistance to reverse engineering, and also find ways to obfuscate better for protocols that are vulnerable to fast reverse engineering. We will also develop reverse engineering tools so that we can construct formal models of protocols and apply formal verification and analysis to find vulnerabilities in such protocols, and certify the products that use proprietary protocols.
In another strand of this work package we plan on developing a safe and secure version of openSSL, and openSSH libraries along with hardware crypto cards which provide coprocessor support for symmetric encryption to the SSL through a new TLS library based on hardware/software co-design. Much of the new implementation architecture will be aimed at improving upon existing implementations from abroad, especially from security perspective. The new TLS library will consider the attacks on the key exchange protocol based on prime number fixing and reuse, and symmetric cryptography would also add certain algorithms which can be selected for highly critical communications. The co-processor based crypto in a hardware/Software mixed solution of SSL implementation will add extra innovation. The product of this research, when embedded in the network implementation of Indian critical sector industries, would render them more secure, free of concerns about Trojans, and backdoors.
Contact
Dr. Pallab Dasgupta
Professor, Department of Computer Science and Engineering
Indian Institute of Technology Kharagpur
Email: pallab[at]cse[DOT]iitkgp[DOT]ernet[DOT]in
Dr. Soumyajit Dey
Assistant Professor, Department of Computer Science and Engineering
Indian Institute of Technology Kharagpur
Email: soumyajit[at]cse[DOT]iitkgp[DOT]ernet[DOT]in
Mr. Antonio Bruto da Costa
Ph.D. Student, Department of Computer Science and Engineering
Indian Institute of Technology Kharagpur
Email: bruto[at]cse[DOT]iitkgp[DOT]ernet[DOT]in