Special Session on Security Verification
Formal Analysis of Security Data Paths in RTL Design
Jamil Mazzawi, Consulting Services Manager, Jasper Design Automation
Recently we have seen an increasing demand in the industrial hardware design to verify security information. Complex system-on-chips such as cellphone, game console, and advanced CPUs contain secure information. This likely leads to vulnerability by unauthorized access to secure data. The potential loss, direct and indirect, is very big. Checking if the secure information can be leaked is hard to achieve in conventional RTL validation methods. In this talk we present how formal can be used to detect unauthorized access to the secure data, by a method called security path verification and analysis.
Jamil Mazzawi is the Consulting Services Manager at Jasper Design Automation. In this role, Jamil is responsible for delivering high-quality verification services to Jasper's customers. Most notably, he is responsible for tackling customer's top verification challenges, for example, low-power verification and hardware security verification. Before he was the Consulting Services Manager, Jamil worked as an Applications Engineer helping Jasper's customers deploy Jasper formal technologies within their teams and flows, mostly by ramping-up their engineers on Jasper's formal technologies.
Jamil has over 19 years of industry experience focused on verification, especially coverage-driven and constrained-random with Specman. He also worked at Ornet, Verisity, Sun Microsystems, and Rambus before starting his career with Jasper Design Automation. He has a B.Sc. in Computer Engineering from Technion-Israel Institute of Technology and an MBA from San Jose State University.
As in previous years, the post-conference proceedings will be published in Springer's Lecture Notes in Computer Science series (LNCS).