A Formal Verification Method To Detect Timing Side Channels In MCU SoCs

A technical paper titled “A New Security Threat in MCUs – SoC-wide timing side channels and how to find them” was published by researchers at University of Kaiserslautern-Landau and Stanford University. Abstract: "Microarchitectural timing side channels have been thoroughly investigated as a security threat in hardware designs featuring shared buffers (e.g., caches) and/or parallelism b... » read more

LLM-Assisted Generation Of Formal Verification Testbenches: RTL to SVA (Princeton)

A technical paper titled “From RTL to SVA: LLM-assisted generation of Formal Verification Testbenches” was published by researchers at Princeton University. Abstract: "Formal property verification (FPV) has existed for decades and has been shown to be effective at finding intricate RTL bugs. However, formal properties, such as those written as System Verilog Assertions (SVA), are time-con... » read more

Formal Verification Best Practices: Investigating A Deadlock

To ensure a design is deadlock free with formal verification, one approach consists in verifying that it is “always eventually” able to respond to a request. The wording is important. Regardless of the current state and the number of cycles we must wait, in the future the design must respond. This translates very nicely using a type of SystemVerilog Assertion called “liveness propertie... » read more

Formally Verifying Data-Oblivious Behavior In HW Using Standard Property Checking Techniques

A technical paper titled “A Scalable Formal Verification Methodology for Data-Oblivious Hardware” was published by researchers at RPTU Kaiserslautern-Landau and Stanford University. Abstract: "The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique... » read more

Formal Verification Of a Sequestered Encryption Architecture

A technical paper titled “Security Verification of Low-Trust Architectures” was published by researchers at Princeton University, University of Michigan, and Lafayette College. Abstract: "Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we... » read more

Formally Modeling A Security Monitor For Virtual Machine-Based Confidential Computing Systems (IBM)

A technical paper titled “Towards a Formally Verified Security Monitor for VM-based Confidential Computing” was published by researchers at IBM Research and IBM T.J. Watson Research Center. Abstract: "Confidential computing is a key technology for isolating high-assurance applications from the large amounts of untrusted code typical in modern systems. Existing confidential computing syste... » read more

New Concepts Required For Security Verification

Verification for security requires new practices in both the development and verification flows, but tools and methodologies to enable this are rudimentary today. Flows are becoming more complex, especially when they span multiple development groups. Security is special in that it is pervasive throughout the development process, requiring both positive and negative verification. Positive ver... » read more

Why It’s So Difficult To Ensure System Safety Over Time

Safety is emerging as a concern across an increasing number of industries, but standards and methodologies are not in place to ensure electronic systems attain a defined level of safety over time. Much of this falls on the shoulders of the chip industry, which provides the underlying technology, and it raises questions about what more can be done to improve safety. A crude taxonomy recently ... » read more

Modification Of An Existing E-Graph Based RTL Optimization Tool As A Formal Verification Assistant

A technical paper titled “Datapath Verification via Word-Level E-Graph Rewriting” was published by researchers at Intel Corporation and Imperial College London. Abstract: "Formal verification of datapath circuits is challenging as they are subject to intense optimization effort in the design phase. Industrial vendors and design companies deploy equivalence checking against a golden or exi... » read more

Hardware-Efficient Approach To Defend Against Fault Attacks

A technical paper titled "Fault Attacks on Access Control in Processors: Threat, Formal Analysis and Microarchitectural Mitigation" was published by researchers at University of Kaiserslautern-Landau. Abstract: "Process isolation is a key component of the security architecture in any hardware/software system. However, even when implemented correctly and comprehensively at the software (SW) le... » read more

← Older posts