CIS Seminars and Events

Spring 2019 Colloquium Series

Unless otherwise noted, CIS lectures are held weekly on Tuesday and/or Thursday from 3:00 p.m. to 4:00 p.m. in Wu and Chen Auditorium, Levine Hall.  For all Penn Engineering events, visit the Penn Calendar.

If you need further information please contact cherylh@cis.upenn.edu.

Thursday, January 17
Steve Swanson
Computer Science & Engineering
University of California, San Diego
"What Should We Do With Persistent Main Memory?"

Read the Abstract and Bio

Abstract: Memory systems are on the verge of a renaissance: Scalable, persistent main memories (e.g., Intel’s 3DXPoint) are the first new technology to enter the upper layers of the memory hierarchy in 50 years. They bring a fundamentally new capability (i.e., persistence), a dramatic increase in capacity, and an array of complications (e.g., asymmetric read and write performance, power limitations, and wear out). This combination of characteristics raises a deceptively simple but fundamental question: What should we do with persistent main memory? In this talk, I will describe several potential answers and the systems my group has built to help understand how different answers affect performance, programmability, and other aspects of system design. I’ll also highlight the central challenges that these memories present and try to summarize what we have learned about them. Finally, I’ll describe what I see as the most interesting avenues for future work.

Bio: Steven Swanson is a professor in the Department of Computer Science and Engineering at the University of California, San Diego and the director of the Non-volatile Systems Laboratory. His research interests include the systems, architecture, security, and reliability issues surrounding heterogeneous memory/storage systems, especially those that incorporate non-volatile, solid-state memories. He has received an NSF CAREER Award, Google Faculty Awards, a Facebook Faculty Award, and been a NetApp Faculty Fellow. He is a co-founder of the Non-Volatile Memories Workshop. In previous lives, he worked on low-power co-processors for irregular applications and building scalable dataflow architectures. He received his Ph.D. from the University of Washington in 2006 and his undergraduate degree from the University of Puget Sound in 1999.

Tuesday, January 29
Caroline Trippel
Department of Computer Science
Princeton University
"Made to Order: Verifying Correctness and Security of Hardware through Event Orderings"

Read the abstract and Bio

Abstract: 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.

Bio: Caroline Trippel is a Ph.D. candidate in the Computer Science Department at Princeton University. She is advised by Professor Margaret Martonosi on her computer architecture dissertation research, specifically on the topic of concurrency and security verification in heterogeneous parallel systems. Her work bridges computer architecture and formal methods and demonstrates the importance of that bridge in specifying and verifying the correct and secure execution of software running on such systems. Trippel has influenced the design of the RISC-V ISA memory consistency model (MCM) both via full-stack MCM analysis of its draft specification and her subsequent participation in the RISC-V Memory Model Task Group; she received recognition for this work via the 2017-2018 NVIDIA Graduate Research Fellowship. Additionally, Trippel has developed a novel methodology and tool that synthesized two new variants of the recently publicized Meltdown and Spectre attacks; this work lead to a funded collaboration with Intel on side-channel attack research. She received her B.S. in Computer Engineering from Purdue University in 2013 and her M.A. in Computer Science from Princeton University in 2015. She will receive her Ph.D. in Computer Science from Princeton University in Spring 2019.

Date TBD
Read the Abstract and Bio

Abstract: Text forthcoming.

Bio: Text forthcoming.

Date TBD
Read the Abstract and Bio

Abstract: Text forthcoming.

Bio: Text forthcoming.

Date TBD
Read the Abstract and Bio

Abstract: Text forthcoming.

Bio: Text forthcoming.