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.


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

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

Pallab Dasgupta

Department of Computer Science and Engineering
Indian Institute of Technology Kharagpur
Email: pallab[at]cse[DOT]iitkgp[DOT]ernet[DOT]in