Sourav Das

I am actively involved in Formal Verification, with a specific focus on multi-property verification and leveraging cutting-edge SAT solvers. My current research centers on integrating various Machine Learning techniques into Formal Verification methodologies. I am particularly intrigued by how these techniques can expedite verification convergence, potentially improving scalability and reducing time-to-market for complex systems and software applications.

• Bifrost: Covert Data Exfiltration from Air-gapped Netoworks via smart bulbs. Finalist in CSAW Embedded Security Challenge, (2018)
• 3rd Prize in Debug the Code, IIT MADRAS (2018)
• Gate Score: 676, AIR: 923 (2017)
• Runners up in Intra-CRIS Hackathon (2017)
• Gate Score: 748, AIR: 425 (2014)

• SHAKTI-MS: A RISC-V Processor for Memory Satefy in C. Shakti-MS is a lightweight RISC-V processor with built-in support for both temporal and spatial memory protection. At runtime, Shakti-MS can detect and stymie memory misuse in C and C++ programs with minimum runtime overheads. The proposed solution uses the novel concepts of fat-pointers that associate pointers with capabilities. It also uses a modified compiler and adds new instructions in the hardware to achieve this low overhead.

Co-authors: Arjun Menon, Hari, Chester Rebeiro, Kamakoti Veezinathan

Url: https://dl.acm.org/doi/10.1145/3316482.3326356

LCTES 2019: Proceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, June 2019

• The CoveRT Approach for Coverage Management in Analog and Mixed Signal Integrated Circuits. Coverage is a key indicator for verification progress, verification closure, and verification sign-off in an integrated circuit design. The notion of coverage management, namely, the use of coverage information across the design hierarchy to identify verification loopholes, is well understood in the digital context, but requires considerable disambiguation in the analog/mixed-signal (AMS) context. This article develops the core artifacts of AMS coverage and presents a comprehensive coverage management approach based on our tool, CoveRT. Our results, gleaned from live industrial designs, demonstrate the benefits of AMS coverage management across the design hierarchy, both in terms of identifying verification gaps, as well as in finding design bugs.

Co-authors: Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Scott Morrison, Sudhakar Surendran, Lakshmanan Balasubramanian

Url: https://ieeexplore.ieee.org/document/9729876

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, March 2022

• : A Comprehensive Verification Planning Framework Leveraging PSS Specifications. CoVerPlan, is a comprehensive verification framework built to explore the power of action inferencing on test models written in Portable Stimulus Standards (PSS). The proposed verification framework leverages a SAT planner to unwind the actual verification flow from the PSS specifications and automatically synthesizes target-specific constraint-random testbenches and formal assertions. CoVerPlan also carries out assertion-based verification of the synthesized properties.

Co-authors: Sayandeep Sanyal, Aritra Hazra, Pallab Dasgupta

Url: https://dl.acm.org/doi/abs/10.1145/3543175

ACM TODAES, June 2022

• PURSE: Property Ordering Using Runtime Statistics for Multi-Property Verification. PURSE is the first tool built on top of the Property Directed Reachability (PDR) proof engine that dynamically reorders the properties on the fly by using the runtime statistics dumped by the PDR proof engine while execution. The idea is to reorder the goals on the fly so that hard goals do not hinder the easy ones from getting solved and then use the solved ones to prove the hard goals.

Co-authors: Aritra Hazra, Pallab Dasgupta, Sudipta Kundu, Himanshu Jain

Design Automation and Test in Europe, March 2024

• Bifrost: Covert Data Exfiltration from Air-gapped Networks via smart bulbs. Bifrost aims to take advantage of the security glitches present in today's smart home appliances or rather IoT devices and exfiltrate data over the air-gapped network. Bifrost hacks a given smart bulb and leaks sensitive information by changing the intensity of the light, or by changing different colors of the bulb. The attack can be generalized as well, for hacking other smart home appliances. Identifying different
• Geographical locations using OS based Side Channel Attacks. Given that each city has some unique characteristics, the amount of memory required to render a map would be different amongst cities. The memory footprints of top 280 location found in Wikipedia were searched in Google Maps and were recorded multiple times to create the database. Now given an unknown city from the list, we created a ranking based metric for identifying it.
• Study of Document Authentication Technique for Copyright Protection using Steganography. The project focused on providing document authentication by hiding certain personal information like signatures, thumb impression, etc within the original document without altering its content. The concept of steganography was used to avoid raising any suspicion among the general audience. So it served the purpose of digital signature without third party users being unaware of it.
• E-Library. The project aimed at digitalizing the college library by providing the admin console and the student console with pre-deterministic rights. The administrator can issue, update, and manage the books present in the library, whereas the students can read e-books and check his/hers current status.

• Bifrost: Covert Data Exfiltration from Air-gapped Networks via smart bulbs. Bifrost aims to take advantage of the security glitches present in today's smart home appliances or rather IoT devices and exfiltrate data over the air-gapped network. Bifrost hacks a given smart bulb and leaks sensitive information by changing the intensity of the light, or by changing different colors of the bulb. The attack can be generalized as well, for hacking other smart home appliances. Identifying different
• Geographical locations using OS based Side Channel Attacks. Given that each city has some unique characteristics, the amount of memory required to render a map would be different amongst cities. The memory footprints of top 280 location found in Wikipedia were searched in Google Maps and were recorded multiple times to create the database. Now given an unknown city from the list, we created a ranking based metric for identifying it.
• Study of Document Authentication Technique for Copyright Protection using Steganography. The project focused on providing document authentication by hiding certain personal information like signatures, thumb impression, etc within the original document without altering its content. The concept of steganography was used to avoid raising any suspicion among the general audience. So it served the purpose of digital signature without third party users being unaware of it.
• E-Library. The project aimed at digitalizing the college library by providing the admin console and the student console with pre-deterministic rights. The administrator can issue, update, and manage the books present in the library, whereas the students can read e-books and check his/hers current status.

• SHAKTI-MS: A RISC-V Processor for Memory Satefy in C. Shakti-MS is a lightweight RISC-V processor with built-in support for both temporal and spatial memory protection. At runtime, Shakti-MS can detect and stymie memory misuse in C and C++ programs with minimum runtime overheads. The proposed solution uses the novel concepts of fat-pointers that associate pointers with capabilities. It also uses a modified compiler and adds new instructions in the hardware to achieve this low overhead.

Co-authors: Arjun Menon, Hari, Chester Rebeiro, Kamakoti Veezinathan

Url: https://dl.acm.org/doi/10.1145/3316482.3326356

LCTES 2019: Proceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, June 2019

• The CoveRT Approach for Coverage Management in Analog and Mixed Signal Integrated Circuits. Coverage is a key indicator for verification progress, verification closure, and verification sign-off in an integrated circuit design. The notion of coverage management, namely, the use of coverage information across the design hierarchy to identify verification loopholes, is well understood in the digital context, but requires considerable disambiguation in the analog/mixed-signal (AMS) context. This article develops the core artifacts of AMS coverage and presents a comprehensive coverage management approach based on our tool, CoveRT. Our results, gleaned from live industrial designs, demonstrate the benefits of AMS coverage management across the design hierarchy, both in terms of identifying verification gaps, as well as in finding design bugs.

Co-authors: Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Scott Morrison, Sudhakar Surendran, Lakshmanan Balasubramanian

Url: https://ieeexplore.ieee.org/document/9729876

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, March 2022

• : A Comprehensive Verification Planning Framework Leveraging PSS Specifications. CoVerPlan, is a comprehensive verification framework built to explore the power of action inferencing on test models written in Portable Stimulus Standards (PSS). The proposed verification framework leverages a SAT planner to unwind the actual verification flow from the PSS specifications and automatically synthesizes target-specific constraint-random testbenches and formal assertions. CoVerPlan also carries out assertion-based verification of the synthesized properties.

Co-authors: Sayandeep Sanyal, Aritra Hazra, Pallab Dasgupta

Url: https://dl.acm.org/doi/abs/10.1145/3543175

ACM TODAES, June 2022

• PURSE: Property Ordering Using Runtime Statistics for Multi-Property Verification. PURSE is the first tool built on top of the Property Directed Reachability (PDR) proof engine that dynamically reorders the properties on the fly by using the runtime statistics dumped by the PDR proof engine while execution. The idea is to reorder the goals on the fly so that hard goals do not hinder the easy ones from getting solved and then use the solved ones to prove the hard goals.

Co-authors: Aritra Hazra, Pallab Dasgupta, Sudipta Kundu, Himanshu Jain

Design Automation and Test in Europe, March 2024

• SHAKTI-MS: A RISC-V Processor for Memory Satefy in C. Shakti-MS is a lightweight RISC-V processor with built-in support for both temporal and spatial memory protection. At runtime, Shakti-MS can detect and stymie memory misuse in C and C++ programs with minimum runtime overheads. The proposed solution uses the novel concepts of fat-pointers that associate pointers with capabilities. It also uses a modified compiler and adds new instructions in the hardware to achieve this low overhead. Co-authors: Arjun Menon, Harikrishnan Unnithan, Chester Rebeiro, Kamakoti Veezinathan. [Accepted in LCTES, June 2019]

• The CoveRT Approach for Coverage Management in Analog and Mixed Signal Integrated Circuits. Coverage is a key indicator for verification progress, verification closure, and verification sign-off in an integrated circuit design. The notion of coverage management, namely, the use of coverage information across the design hierarchy to identify verification loopholes, is well understood in the digital context, but requires considerable disambiguation in the analog/mixed-signal (AMS) context. This article develops the core artifacts of AMS coverage and presents a comprehensive coverage management approach based on our tool, CoveRT. Our results, gleaned from live industrial designs, demonstrate the benefits of AMS coverage management across the design hierarchy, both in terms of identifying verification gaps, as well as in finding design bugs. Co-authors: Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Scott Morrison, Sudhakar Surendran, Lakshmanan Balasubramanian. [Accepted in TCAD, March 2022]

• : A Comprehensive Verification Planning Framework Leveraging PSS Specifications. CoVerPlan, is a comprehensive verification framework built to explore the power of action inferencing on test models written in Portable Stimulus Standards (PSS). The proposed verification framework leverages a SAT planner to unwind the actual verification flow from the PSS specifications and automatically synthesizes target-specific constraint-random test benches and formal assertions. CoVerPlan also carries out assertion-based verification of the synthesized properties. Co-authors: Sayandeep Sanyal, Aritra Hazra, Pallab Dasgupta. [Accepted in ACM TODAES, June 2022]

• PURSE: Property Ordering Using Runtime Statistics for Multi-Property Verification. PURSE is the first tool that dynamically reorders the properties on the fly by using the runtime statistics dumped by the Property Directed Reachability (PDR) proof engine while execution. The idea is to reorder the goals on the fly after every iteration based on the statistics dumped from the PDR proof engine, so that hard goals do not hinder the easy ones from getting solved. Co-authors: Aritra Hazra, Pallab Dasgupta, Sudipta Kundu, Himanshu Jain. [Accepted in Design Automation and Test in Europe, March 2024]

• Bifrost: Covert Data Exfiltration from Air-gapped Networks via smart bulbs. Bifrost aims to take advantage of the security glitches present in today's smart home appliances or rather IoT devices and exfiltrate data over the air-gapped network. Bifrost hacks a given smart bulb and leaks sensitive information by changing the intensity of the light, or by changing different colors of the bulb. The attack can be generalized as well, for hacking other smart home appliances. Identifying different
• Geographical locations using OS based Side Channel Attacks. Given that each city has some unique characteristics, the amount of memory required to render a map would be different amongst cities. The memory footprints of top 280 location found in Wikipedia were searched in Google Maps and were recorded multiple times to create the database. Now given an unknown city from the list, we created a ranking based metric for identifying it.
• Study of Document Authentication Technique for Copyright Protection using Steganography. The project focused on providing document authentication by hiding certain personal information like signatures, thumb impression, etc within the original document without altering its content. The concept of steganography was used to avoid raising any suspicion among the general audience. So it served the purpose of digital signature without third party users being unaware of it.
• E-Library. The project aimed at digitalizing the college library by providing the admin console and the student console with pre-deterministic rights. The administrator can issue, update, and manage the books present in the library, whereas the students can read e-books and check his/hers current status.

• SHAKTI-MS: A RISC-V Processor for Memory Satefy in C. Shakti-MS is a lightweight RISC-V processor with built-in support for both temporal and spatial memory protection. At runtime, Shakti-MS can detect and stymie memory misuse in C and C++ programs with minimum runtime overheads. The proposed solution uses the novel concepts of fat-pointers that associate pointers with capabilities. It also uses a modified compiler and adds new instructions in the hardware to achieve this low overhead. Co-authors: Arjun Menon, Harikrishnan Unnithan, Chester Rebeiro, Kamakoti Veezinathan. [Accepted in LCTES, June 2019]

• The CoveRT Approach for Coverage Management in Analog and Mixed Signal Integrated Circuits. Coverage is a key indicator for verification progress, verification closure, and verification sign-off in an integrated circuit design. The notion of coverage management, namely, the use of coverage information across the design hierarchy to identify verification loopholes, is well understood in the digital context, but requires considerable disambiguation in the analog/mixed-signal (AMS) context. This article develops the core artifacts of AMS coverage and presents a comprehensive coverage management approach based on our tool, CoveRT. Our results, gleaned from live industrial designs, demonstrate the benefits of AMS coverage management across the design hierarchy, both in terms of identifying verification gaps, as well as in finding design bugs. Co-authors: Sayandeep Sanyal, Pallab Dasgupta, Aritra Hazra, Scott Morrison, Sudhakar Surendran, Lakshmanan Balasubramanian. [Accepted in TCAD, March 2022]

• : A Comprehensive Verification Planning Framework Leveraging PSS Specifications. CoVerPlan, is a comprehensive verification framework built to explore the power of action inferencing on test models written in Portable Stimulus Standards (PSS). The proposed verification framework leverages a SAT planner to unwind the actual verification flow from the PSS specifications and automatically synthesizes target-specific constraint-random test benches and formal assertions. CoVerPlan also carries out assertion-based verification of the synthesized properties. Co-authors: Sayandeep Sanyal, Aritra Hazra, Pallab Dasgupta. [Accepted in ACM TODAES, June 2022]

• PURSE: Property Ordering Using Runtime Statistics for Multi-Property Verification. PURSE is the first tool that dynamically reorders the properties on the fly by using the runtime statistics dumped by the Property Directed Reachability (PDR) proof engine while execution. The idea is to reorder the goals on the fly after every iteration based on the statistics dumped from the PDR proof engine, so that hard goals do not hinder the easy ones from getting solved. Co-authors: Aritra Hazra, Pallab Dasgupta, Sudipta Kundu, Himanshu Jain. [Accepted in Design Automation and Test in Europe, March 2024]

• Bifrost: Covert Data Exfiltration from Air-gapped Networks via smart bulbs. Bifrost aims to take advantage of the security glitches present in today's smart home appliances or rather IoT devices and exfiltrate data over the air-gapped network. Bifrost hacks a given smart bulb and leaks sensitive information by changing the intensity of the light, or by changing different colors of the bulb. The attack can be generalized as well, for hacking other smart home appliances. Identifying different
• Geographical locations using OS based Side Channel Attacks. Given that each city has some unique characteristics, the amount of memory required to render a map would be different amongst cities. The memory footprints of top 280 location found in Wikipedia were searched in Google Maps and were recorded multiple times to create the database. Now given an unknown city from the list, we created a ranking based metric for identifying it.
• Study of Document Authentication Technique for Copyright Protection using Steganography. The project focused on providing document authentication by hiding certain personal information like signatures, thumb impression, etc within the original document without altering its content. The concept of steganography was used to avoid raising any suspicion among the general audience. So it served the purpose of digital signature without third party users being unaware of it.
• E-Library. The project aimed at digitalizing the college library by providing the admin console and the student console with pre-deterministic rights. The administrator can issue, update, and manage the books present in the library, whereas the students can read e-books and check his/hers current status.