Talks & Seminars
Title: Towards Secure Computing Systems From The Bottom Up
Dr. Pramod Subramanyam, University of California, Berkeley
Date & Time: July 26, 2017 15:30
Venue: Conference Room, C Block, 01st Floor, Dept. of CSE, Kanwal Rekhi (KReSIT) Bldg.
Today's computing devices store and process an enormous amount of security-critical and privacy-sensitive data. This data is a lucrative target for cybercriminals and other malicious actors. As evidenced by the relentless parade of security breaches at various institutions, building secure computing platforms that can protect sensitive data remains a key challenge in computer science. Hardware security is especially important in this battle for two reasons. First, hardware is one of the roots of trust in a computing system. Security protections in software may be invalidated by faulty hardware. Second, system-designers are now increasingly moving security-critical functionality from application/system software to hardware/firmware in order to combat the perceived insecurity of software. I argue that in order to design secure hardware/firmware platform, we must address three separate but related challenges: (i) platform modeling and abstraction, (ii) security property specification, and (iii) scalable property verification. In this talk, I will describe our methodology for security verification of modern systems-on-chip (SoC) platforms which attempts to address the above three challenges. We first introduce the notion of an instruction-level abstraction (ILA) -- an abstraction that captures firmware-visible behavior of SoC hardware. The ILA enables scalable verification and a clean separation of concerns between hardware and firmware verification. We introduce semi-automated techniques for the synthesis of ILAs from partial descriptions known as templates. We describe methods for specifying and verifying system-level security properties using the ILA. The ILA-based verification methodology has helped find several bugs in RTL implementations, simulators and firmware of open-source and commercial SoC designs. I will provide a brief overview of similar challenges in a slightly different application domain and describe our recent work on the formalization, modeling and verification of security of enclave platforms like Intel SGX and MIT Sanctum. I conclude with some thoughts on future research directions in hardware security.
Speaker Profile:
Pramod Subramanyan is a postdoctoral scholar in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley where he works with Prof. Sanjit Seshia. His research addresses hardware and firmware security concerns using formal algorithms and analyses. He obtained his Ph.D. from the Department of Electrical Engineering at Princeton University under the guidance of Prof. Sharad Malik. Prior to joining Princeton, Pramod obtained an M.Sc. (Engg.) degree from the Indian Institute of Science and a B.E. degree from the R. V. College of Engineering, Bangalore. Before his doctoral studies, Pramod was also a software engineer at National Instruments and a hardware design engineer at AMD.
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback