Prof Trippel
Abstract: Hardware-software (HW-SW) contracts are critical for high-assurance computer systems design and an enabler for software design/analysis tools that find and repair hardware-related bugs in programs. Emerging security contracts define what program data is susceptible to leakage via hardware side-channels and what speculative control- and dataflow is possible at runtime. However, these contracts and the analyses they support are useless if we cannot guarantee microarchitectural compliance, which is a “grand challenge.” Even for mature contracts, comprehensively verifying that a complex microarchitecture implements some abstract contract is a time-consuming endeavor involving teams of engineers, which typically requires resorting to incomplete proofs.

In this talk, I will present our work on: synthesizing security contracts from processor specifications written in Verilog; designing compiler approaches parameterized by these contracts; and updating hardware microarchitectures to support scalable verification and efficient security-hardened programs. I will conclude by outlining remaining challenges in attaining the vision of verified software security down to gates.

Prof Achour
Abstract: Over the years, there has been a proliferation of novel computing paradigms, such as quantum computation, hyperdimensional computing, p-computing, and analog computation, that promise to revolutionize certain classes of computations. These paradigms exhibit unique computational properties and are efficiently implementable using emerging and analog hardware technologies.

In this talk, I will discuss the benefits of rethinking how computation is done, the challenges associated with effectively using new computational paradigms, and provide examples of how software techniques and tools can help overcome some of these challenges. We will overview software techniques my group has developed for effectively using analog, quantum, and hyperdimensional computing paradigms and co-optimizing computations that target these paradigms with emerging and analog hardware technologies