Feb 25

Computer Security for Emerging Technologies

11:40 AM to 12:40 PM

CS Department 451

Earlance Fernandes, University of Washington

As our world becomes more computerized, security and privacy takes on a prominent role in allowing us to enjoy the benefits of new technologies without the risks. Addressing the new challenges that come with this role requires a change in how we approach and solve problems in computer security. My vision is that we must view computer security as a whole-system property ranging from the physical-layer right up to applications and end-users. In line with this vision, my approach to computer security involves formulating the right security problem to work on, addressing design-level issues by constructing strong defenses at the appropriate layer of abstraction, and challenging common assumptions to understand realistic threats. In this talk, I will give several examples of my approach and vision, focusing on emerging technologies that span the digital-to-physical interface. I will cover technical results at various level of abstraction, including analysis techniques that found exploitable design-level vulnerabilities in closed-source smart home platforms, a new design for trigger-action platforms that provides strong integrity guarantees, and an analysis of how realistic attacks on machine learning can occur in the physical world. Finally, I will share my vision of the future of security and privacy research in an increasingly connected world.

Feb 27

Hardware accelerators for deep learning: a proving ground for specialized computing

11:40 AM to 12:40 PM

CS Department 451

Brandon Reagan

The computing industry has a power problem: the days of ideal power-process scaling are over, and chips now have more devices than can be fully powered simultaneously, limiting performance. New architecture-level solutions are needed to continue scaling performance, and specialized hardware accelerators are one such solution. While accelerators promise to provide orders of magnitude more performance per watt, several challenges have limited their wide-scale adoption.

Deep learning has emerged as a sort of proving ground for hardware acceleration. With extremely regular compute patterns and wide-spread use, if accelerators can’t work here, then there’s little hope elsewhere. For accelerators to be a viable solution they must enable computation that cannot be done today and demonstrate mechanisms for performance scaling, such that they are not a one-off solution. This talk will present deep learning algorithm-hardware co-designs to answer these questions and identify the efficiency gap between standard hardware design practices and full-stack co-design to enable deep learning to be used with little restriction. To push the efficiency limits, this talk will introduce principled unsafe optimizations. A principled unsafe optimization changes how a program executes without impacting accuracy. By breaking the contract between the algorithm, architecture, and circuits, efficiency can be greatly improved. To conclude, future research directions centering around hardware specialization will be presented: accelerator-centric architectures and privacy-preserving cloud computing.

Mar 04

Made to Order : Verifying Correctness and Security of Hardware through Event Orderings

11:40 AM to 12:40 PM

CS Department 451

Caroline Trippel, Princeton University

Correctness and security problems in modern computer systems can result from problematic hardware event orderings and interleavings during an application’s execution. Since hardware designs are complex and since a single user-facing instruction can exhibit a variety of different hardware execution sequences, analyzing and verifying systems for correct event orderings is challenging. My work addresses these challenges by combining hardware architecture and systems approaches with formal methods to support the specification, analysis, and verification of implementation-aware event ordering scenarios, with the specific goal of automatically synthesizing implementation-aware programs capable of violating correctness or security guarantees. In this talk, I will present two formal, early-stage verification tools and techniques rooted in this approach. TriCheck conducts axiomatic full-stack memory consistency model (MCM) verification (from high-level programming languages down through hardware implementations). Using rigorous and efficient formal approaches, TriCheck identified flaws in RISC-V’s draft MCM specification and two counterexamples to a previously proven-correct compiler mapping scheme from C11 to IBM Power and ARMv7. Noting that MCM and security analysis are amenable to similar approaches, CheckMate uses related axiomatic techniques to evaluate susceptibility of a hardware design and its related system support to formally-specified classes of security exploits; in response, it synthesizes proof-of-concept exploit code when a design is susceptible. CheckMate automatically synthesized programs representative of Meltdown and Spectre attacks as well as new exploits, MeltdownPrime and SpectrePrime, that I have demonstrated on Intel hardware.

Mar 06

CS Faculty Recruiting Colloquium - Sophia Shao

11:40 AM to 12:40 PM

CS Department 451

Mar 08

Theory Seminar - Shuchi Chawla

1:00 PM to 2:00 PM

CS conference room (CSB 453)

Shuchi Chawla