Security in the Internet of Things Space
Centre of Excellence in Cyber Systems and Information Assurance, Indo-Japanese Collaborative Research Project. Department of Science and Technology, Government of India. March 2017-February 2022. INR 14,482,500.Sanjiva Prasad (PI.) [Collaboration: Kyushu University], Madhukar Yerraguntla
Secure Composition in Synchronous Dataflow systems
Synchronous reactive data flow is a paradigm that provides a high-level abstract programming model for embedded and cyber-physical systems, including the locally synchronous components of IoT systems. Security in such systems is severely compromised due to low-level programming, ill-defined interfaces and inattention to security classification of data. By incorporating a Denning-style lattice-based secure information flow framework into a synchronous reactive data flow language, we provide a framework in which correct-and-secure-by-construction implementations for such systems can be specified and derived. In particular, we extend the Lustre programming framework with a security type system. The work is currently being formalized in Coq over Vèlus development.
Collaborative Neuro-Engineering Platform for Excellence in Innovation and Translational Research
Department of Biotechnology, Ministry of Science and Technology, Government of India. March 2018-February 2023. INR 17,467,000. Total Budget INR 65,716,000.Sanjiva Prasad (Co-PI.) [Collaboration: All India Institute of Medical Sciences (AIIMS)]
Dynamic Verification of C/C++11 Concurrency
The permissible behaviors under C/C++11 model are complex, making it challenging to capture the semantics for a comprehensive analysis. The aim of this work is to create a sound, efficient and scalable program analysis technique to detect races and property violations in a C/C++11 source program.
Abstract Interpretation of Concurrent Programs
Verification of parallel systems is a complex exercise as large state space created due to thread interleavings makes it hard to verify the properties of such parallel systems. The problem becomes even harder in case of parallel programs executed under relaxed memory models. This work focuses on precise thread- modular abstract interpretation based approach for verifying properties of concurrent programs under relaxed memory model.Efficient compilation of network DSLs
Recently, the software switches are taking the center stage of replacing the traditional middleboxes in networking for their relative flexibility in development, deployment, and maintenance. DSLs for programming software switches have become an attractive choice, but the challenge of achieving line-rate for different workloads and platforms still persists. Focusing towards the development of the right compiler framework for optimization could bridge this gap between flexibility and performance. We address the problem of writing an ideal compiler for efficiently mapping a high-level protocol specification to the underlying target architecture.
Safety Verification of Li-ion Batteries
Li-ion battery systems are part of almost every cyber-physical system. Their high energy to weight ratio makes them very portable and at the same time poses many risks. The charging and discharging patterns should be followed strictly. This work tries to answer whether a charge-discharge pattern is "safe" on a battery through formal means.Synthesis and Superoptimization
An automatic "peephole superoptimizer", an idea that is described in detail in this paper on Automatic Generation of Peephole Superoptimizers. While this work automatically generated peephole optimizations through search-based techniques, later work on binary translation extended these ideas to automatically generate translations from one ISA (PowerPC) to another (x86). In current work, we have been generalizing these ideas to automatically generate translations from LLVM IR to x86 ISA. We have also generalized the nature of these translations to allow reasoning about loops and aliasing, two very important features that enable effective compiler optimizations.