Formally Verifying Processor Security
November 20, 2019
Intel has had a couple of major events that totally changed their attitude to verification. The first was in 1994 when they had the Pentium floating-point divide bug and management said “don’t ever let this happen again”. In 1996, they started proving properties of the Pentium processor FPU.
Then, a couple of years ago, the side-channel vulnerabilities like Spectre were discovered. These didn't just affect Intel, it turned out every modern CPU had the same problem hiding in plain view for 20 years. Basically, the vulnerability plays on speculative execution making memory references and then being able to discover which memory elements were accessed, even though the speculative execution got abandoned.
Related Semiconductor IP
- RISC-V CPU IP
- AES GCM IP Core
- High Speed Ethernet Quad 10G to 100G PCS
- High Speed Ethernet Gen-2 Quad 100G PCS IP
- High Speed Ethernet 4/2/1-Lane 100G PCS
Related Blogs
- Verifying Processor Security, Part 2
- Formally verifying protocols
- Arm receives first high assurance Common Criteria security certification for soft processor IP
- Commodity processor IP !?!
Latest Blogs
- Why Choose Hard IP for Embedded FPGA in Aerospace and Defense Applications
- Migrating the CPU IP Development from MIPS to RISC-V Instruction Set Architecture
- Quintauris: Accelerating RISC-V Innovation for next-gen Hardware
- Say Goodbye to Limits and Hello to Freedom of Scalability in the MIPS P8700
- Why is Hard IP a Better Solution for Embedded FPGA (eFPGA) Technology?