Formal Methods for Safety-Critical System Design and Validation:
Formal methods specify rigorous theoretical and mathematical models to design software and hardware systems and use formal techniques to validate and certify the design behaviors, ensuring its correctness, power management, reliability, security, quality and robustness attributes. We primarily aim to design automated frameworks for the following aspects:
(a) Functional correctness of integrated circuit designs during various phases (both in pre-silicon as well as post-silicon) leveraging simulation, formal as well as semi-formal techniques
(b) Comprehensive verification of the power management strategy for integrated circuits involving the digital power manager orchestrating the analog power control circuitry
(c) Reliability and robustness analysis of safety-critical systems from formal specifications of spatial and temporal redundancy artefacts, properties of the error-free system, error probabilities of the control components, and reliability targets
Computer-Aided Design (CAD) for Security:
VLSI designs and integrated circuits are manufactured using several CAD frameworks where many challenging algorithmic problems need to be solved, including design synthesis, floor-planning, placement and routing, to deliver a final chip. We primarily focus on the following aspects:
(a) Vulnerability assessment of cryptographic primitives in secure cipher designs with respect to fault attacks and synthesis of automatic countermeasures to mitigate security flaws in cipher algorithms as well as their hardware or software implementations
(b) Developing strong physically unclonable function (PUF) designs and its compositions which are resilient to machine learning attacks, leveraging CAD based testability and formal learnability analysis frameworks, justifying the responsiveness, unclonability, reliability, correlation and learnability factors of PUFs
Robust Explainability of Machine Learning Models:
Explainability is becoming one of the key needs for widespread adoption of ML approaches in safety-critical applications. We primarily target to explore and devise approaches for comprehensive interpretability as well as ensure robustness of trained ML models so that it cannot be fooled or manipulated by adversarial/malicious perturbations.
Principal Investigator
- A Formal Coverage Management Framework for AMS Design Verification (GRC Proposal ID: P32524)
- Machine Learning at the Digital-Analog Boundary - A Contract Assurance Framework based on AMS Assertions
- Scalable Formal Property Verification Leveraging Property Grouping and Ordering
- Synopsys CAD Laboratory Phase III
- The Qualcomm Faculty Award (QFA) 2021
Co-Principal Investigator
- Exploring Human and Machine Cognition: Building a Learning Analytics Portal
of AI Assisted Problem Solving Models for Visuo-Spatial Tasks (1817_ZBSA) Department of Science and Technology (DST)
- Formal Methods for Verification of Power Management in Mixed Signal Designs INTEL CORPORATION, USA.
- Secure Resource-Constrained Communication Framework for Tactical Networks Using Physically Unclonable Functions (SeRFPUF) Directorate of Futuristic Technology Management (DFTM), Defence Research and Development Organisation, Ministry of Defence
- Specialized Training on Formal Verification Synopsys Inc.
Ph. D. Students
Das Adhikary Debjyoti Tushar
Area of Research: Artificial Intelligence
Durba Chatterjee
Area of Research: Cryptography
Madhumanti Bhattacharyya
Area of Research: Cognitive Neuropsychology
Madhusudhan K N
Area of Research: ML for CAD
Sourav Das
Area of Research: Design Verification
