Scaling Hardware Security Property Generation

One of the biggest challenges in hardware security verification is developing formal properties that can subsequently be verified by automated tools. This is a difficult and time-consuming task typically assigned to security verification engineers that must manually sort through hundreds of thousands of lines of a hardware description.

Isadora Duncan By Arnold Genthe - http://snap361.net/ig-tag/arnoldgenthe/, Public Domain, https://commons.wikimedia.org/w/index.php?curid=76948922

Our recent article in IEEE Security & Privacy Special Issue on Formal Methods at Scale describes our research on developing Isadora – a tool that automates the property generation process for information-flow properties that are critical to the security of hardware designs. Isadora combines information flow tracking with specification mining to help automate the challenging security verification process. Congrats to the authors: Calvin Deutschbein, Andy Meza, Francesco Restuccia, Ryan Kastner, and Cynthia Sturton.

Olivia Weng Named NSF Graduate Research Fellow

Congratulations to Olivia Weng for being awarded a National Science Foundation Graduate Research Fellowship. The NSF GRF is one of the most prestigious graduate fellowships in the US. The fellowship will fund Liv for the remainder of her PhD allowing her to continue her research on the co-design of efficient, fault-tolerant computer architectures for applications in high-energy physics. One example is the Large Hadron Collider, where physicists need hardware that will process millions of particle collisions per second. Her research will allow their hardware, and the machine learning software that runs on it, to meet these intense computing demands while handing faults that are inherent in such sensors.

Smartfin turns Surfers into Citizen Scientists

Smartfin is an oceanographic sensor–equipped surfboard fin and citizen science program aimed to provide an increase of coastal ocean observations. Smartfins are used by surfers and paddlers in surf zone and nearshore regions to provide valuable oceanographic data in these challenging to sample ecosystems. Smartfin measures temperature, motion, and wet/dry sensing, GPS location, and cellular data transmission capabilities for the near-real-time monitoring of coastal physics and environmental parameters.

Over 300 Smartfins have been distributed around the world and have been in use for up to five years. The technology has been proven to be a useful scientific research tool in the coastal ocean—especially for observing spatiotemporal variability, validating remotely sensed data, and characterizing surface water depth profiles when combined with other tools—and the project has yielded promising results in terms of formal and informal education and community engagement in coastal health issues with broad international reach.

Our recent research article in the Continental Shelf Research journal describes the technology, the citizen science project design, and the results in terms of natural and social science analyses. We also discuss progress toward our outreach, education, and scientific goals. Congrats to Phil Bresnahan and all the authors!

Sherlock: Quickly Understanding Design Spaces

Design space exploration aims to quickly determine the design parameters that yield the best results. In software, the designer must set algorithmic and performance parameters, e.g., thresholds, bounds, and other input parameters that provide the best output in terms of accuracy and runtime. In hardware design, the designer must determine parameters related to pipelining, memory architecture, and data types to give the best tradeoff between resource usage and performance. In both cases, one wants to quickly understand the relationship between the input and outputs and find the Pareto set of designs.

Sherlock is a DSE framework that can handle multiple conflicting optimization objectives and aggressively focuses on finding Pareto optimal solutions. Sherlock integrates a model selection process to choose the regression model that helps reach the optimal solution faster. Sherlock designs a strategy based around the Multi-Armed Bandit (MAB) problem, opting to balance exploration and exploitation based on the learned and expected results. Sherlock can decrease the importance of models that do not provide correct estimates, reaching the optimal design faster. Sherlock is capable of tailoring its choice of regression models to the problem at hand, leading to a model that best reflects the application design space

Sherlock: A Multi-Objective Design Space Exploration Framework” was recently published in the ACM Transactions on Design Automation of Electronic Systems (TODAES). Congrats to the authors Quentin Gautier, Alric Althoff, Chris Crutchfield, and Ryan Kastner. The Sherlock algorithm was also released as open-source. We plan to use it in the future to tune machine learning models for optimized hardware implementations and tune algorithmic parameters for aerial tracking project. We hope that others will find is similarly useful!

CSE Postdoc Fellow

Dr. Francesco Restuccia was awarded a UCSD CSE Postdoc Fellowship to return to UCSD to develop safe and secure system-on-chip architectures.

Francesco is very familiar with UCSD (and vice versa). He spent about 9 months here as a visiting PhD student from January – August 2020. Despite much of his time here being under lockdown, he was incredibly productive. Francesco developed the Aker security verification framework for system on a chip (SoC) access control that was published in ICCAD 2021. Additionally, Francesco worked on another project to develop a makeshift ventilator system in response to the pandemic (see IEEE Embedded Systems Letter for more info).

Francesco will continue his work on developing safe and secure electronic systems, in particular, we aim to explore the use of program synthesis for secure system generation in collaboration with Sean Gao and Nadia Polikarpova. Be on the look out for some more VeriSketch-like research lead by Francesco.

Welcome back Francesco!

Spying on Your FPGA Neighbors

Amazon, Baidu, Microsoft, and other cloud providers now allow one to rent FPGAs and use them to implement powerful and efficient custom architectures for machine learning, video transcoding, encryption, networking, and other high throughput computations. Those FPGAs are large, and quite very expensive, which brings about the natural question: can we virtualize the FPGA across multiple users and maximize their usage? And more importantly, what are the security implications of two tenants sharing the same physical FPGA device?

In our DAC 2021 paper “Classifying Computations on Multi-Tenant FPGA“, we show that a co-tenant can implement a relatively simple circuit time-to-digital converter (TDC) on one part of the FPGA and use that to determine types of computation occurring on another part of the FPGA. The TDC measures small changes in how a signal propagates through a carry chain. If the co-tenant computation is using a lot of power, this creates a side channel via the power supply rail that will slow down the propagation of the signal in the carry chain. We show that his subtle information can be used to

This includes determining if there is another co-tenant, if that co-tenant is performing encryption, whether the co-tenant is utilizing a soft processor, and other questions that violate the confidentiality of the co-tenant. This a necessary precursor for performing attacks in a virtualized FPGA environment, where an attacker must identify a co-located core before performing an attack, or defending against them, where a provider recognizes malicious cores and terminates service

The work was a broad collaboration across several universities. It was lead by Dustin Richmond (UW post-doc) and includes Mustafa Gobulukoglu (UCSD BS/MS now at Northrop Grumman), Colin Drewes (UCSD BS/MS), and Bill Hunter (Georgia Tech Research Institute).

DAC Under-40 Innovator Award

Kastner Research Group alum Dr. Jason Oberg was given the DAC Under-40 Innovators Award. The award recognizes the top young innovators who have made a significant impact in the field of electronics design and automation.

Jason receiving the Under-40 Innovator Award at DAC 2021

Jason is a leader in the hardware security community. Jason’s PhD work helped lay the foundation for hardware information flow tracking. After his PhD, he commercialized this research as co-founder and CEO of Tortuga Logic. Hardware information flow tracking is now a key part of hardware security validation used in top semiconductor companies in a large part due to Jason’s strategic and technical guidance. Jason is currently is CTO at Tortuga, and continues to drive many of the innovations there and in the broader hardware security community.

Floppy-haired Jason at FCCM 2010.

I met Jason at UC Santa Barbara back when I was a professor there. Jason was a floppy-haired surfer fresh from Hawaii, but also an outstanding undergraduate researcher. He worked with Bridget Benson in developing the early version of the AquaModem. Shortly thereafter, I moved to UC San Diego and convinced Jason to follow me there for his PhD. Jason worked on a lot of different topics. He eventually settled on hardware security.

Jason’s hair has gotten a lot less floppy, but the psyche still remains. I have thoroughly enjoyed working with him over the years, and look forward to all the great things that he will undoubtedly do in the future.

iSTELLAR and Aker at ICCAD

Our group presented two papers related to hardware security at the International Conference on Computer-Aided Design (ICCAD). ICCAD is a top-tier conference in electronic design automation. There is an increasing emphasis on hardware security at ICCAD (and most other hardware design research venues) in the past years.

Prof. Jeremy Blackstone presented our group’s first paper: iSTELLAR: intermittent Signature aTtenuation Embedded CRYPTO with Low-Level metAl Routing. iSTELLAR presents a defense against electromagnetic and power attacks on that combines circuit-level and physical-level mitigations from STELLAR with notion of computational blinking. The end result is a flexible defense that enables a tradeoff between power consumption with leakage mitigation. The work was done in collaboration with Prof. Shreyas Sen (Purdue), Dr. Debayan Das (Purdue/Intel), and Dr. Alric Althoff (Tortuga Logic).

Aker — an Egyptian god that guards the netherworld. Image by Jeff Dahl – Own work, CC BY-SA 4.0

Our group’s second paper — Aker: A Design and Verification Framework for Safe and Secure SoC Access Control — was presented by Andy Meza. Aker is a design and security verification framework for system on chip access control. Aker provides flexible hardware access control wrappers that monitor memory accesses. And it provides an extensible security verification environment that can generate a variety of hardware security based upon the threat model. This work was done in collaboration with Dr. Francesco Restuccia (Scuola Superiore Sant’Anna Pisa and soon to be UCSD!). The hardware designs and security properties are released for open use in our Aker repository.

Congrats to all the authors!

Related Links: iSTELLAR paper, Aker paper, Aker Repository

An Unconventional, Unexpected, Outstanding PhD

Dr. Alireza Khodamoradi successfully defended his PhD thesis “Reshaping Deep Neural Networks for Efficient Hardware Inference”. Ali’s PhD has been unconventional in many ways — starting from his admission into UCSD, his unrelenting desire to get a PhD, and his ability to constantly surprise and impress.

Ali’s UCSD journey started almost a decade ago. He was working at the time in a state prison and applied for the WES MAS in the first year of that program. He was rejected. As soon as he was notified of his rejection, Ali contacted me (as WES program director) asked what he could do to get in. I told him to take some UCSD Extension classes as I tell all students in this position.

Hiking to Shadow Lake during the Kastner Research Group Retreat.

For the majority of rejected candidates, they ignore this advice and I never see them again. Ali is unconventional. Not only did he enroll in classes, he also wanted to do some research. I gave him the opportunity to work in our Engineers for Exploration project to demonstrate his skills and more important show us that he was ready and willing to excel in a top graduate program. He volunteered as a researcher and did some really fantastic work as a researcher in the Intelligent Camera Trap project and eventually became the leader of the Angry Birds projects.

The following year, he applied again to the MAS program. He was accepted!

During the WES MAS program, Ali told me that he wanted to do a PhD. I told him that this was very unlikely, that it was not the intended path for WES MAS students, that it would be very challenging to transfer into the PhD program, and that there was no precedent for this. I told him that if he really wanted this, he had to continue to do well in the program and excel in research. Honestly, I did not think that he would get into the PhD program. Again, Ali surprised and took the unconventional path. He become the first WES MAS student to be placed into the PhD program. To date, he is still one of only two WES MAS students to go on to a PhD (and the only one to finish the PhD).

Ali is an amazing educator. He played an integral role in the development of much of the core material of the WES MAS program. He made substantial contributions to the curriculum in my HLS class, but also other embedded classes. He TA’ed almost his entire PhD career, mostly because the program would not have survived without him.

Ali is an outstanding system builder. His work always had an applied aspect. He was a magician at getting the FPGA tools to work and building complete systems. During his PhD, he worked at Cognex and Xilinx to develop cutting edge technologies used in real-world scenarios.

Finally, and not to be overlooked, Ali is a stellar researcher. His PhD research made fundamental advances in hardware accelerated systems for spiking neural networks and for reshaping deep neural networks for implementation on FPGAs. This research was motivated by his time at Xilinx Research Labs where he spent the last 6 months of his PhD. This experience put a focus on Ali’s thesis while allowing him to continue to work on important and industrially relevant research problems. And it got him a full-time job after graduation.

I’ve learned a few things about Ali. First, never judge a book by its cover. Can a telecommunications engineer at a prison get a PhD? Ali showed it is possible. Second, never bet against Ali. You will likely lose this bet. Third, unconventional routes may not be the fastest routes, but they are often the most rewarding.

Congrats Dr. Khodamoradi!

Jeremy Blackstone: Mountaineer, UCSD CSE PhD, and Howard Professor

Congratulations to Jeremy Blackstone for successfully defending his PhD thesis! Jeremy’s PhD research focused on mitigating hardware side channels – a powerful class of security vulnerabilities that exploits the side effects of physically performing a computation. Jeremy’s research focused on the idea of “blinking”, which determines when to turn on/off side channel attack mitigation strategies. The goal is to use the mitigations during the most important time periods and turn them off during less vulnerable times in order to make the system more efficient. This provides the ability to tradeoff between security, performance, power consumption, and other important objectives.

Jeremy has been associated with our research group for a long time. He was a member of our first Engineers for Exploration Summer REU program in Summer 2013 when he was an undergraduate at Howard University. The following summer, he came to UCSD again and this time working with Dustin Richmond on the Tinker project. He was funded to participate in the summer research programs as part of the UCSD Howard Partnership for Graduate Success — a UC HBCU-funded initiative led by Profs. Gentry Patrick in Biological Sciences and Gary Cottrell in Computer Science and Engineering. These two summer research experiences were the key factor in recruiting Jeremy to UCSD. Jeremy would have otherwise not been interested in UCSD without spending the summer in San Diego. And I would have not gotten to know Jeremy and would have been less likely to consider his application and give him an offer.

Jeremy started his his PhD in 2015. During our group retreat Fall 2015, we did a challenging group hike in Mammoth Lakes scrambling up boulders for hundreds of meters near the Crystal Crag. The group picture was taken at the top of that scramble. Jeremy was not an experienced hiker and I did a very poor job of warning him (and others in the group) about the challenges of the hike. It may be hard to tell, but Jeremy was not very happy in this picture (or generally during the hike). In a lot of ways this summarizes a PhD journey. You don’t really know what you are getting into, it is very difficult, sometimes your advisor fails to warn you of pending challenges, but when you make it, you have done things that have never been done before.

Jeremy eventually recovered from that hike, and settled in on hardware security as a PhD topic. He worked with many different people and different topics over his PhD career. His published extensively with people within our group (e.g., Wei Hu, Alric Althoff, Dustin Richmond), at the University of Washington (Michael Taylor, Dustin Richmond), and at Purdue (Shreyas Sen, Debayan Das). Jeremy is clearly a multidisciplinary and collaborative researcher.

After graduation, Jeremy started as an assistant professor in the Department of Electrical Engineering and Computer Science at Howard University. Jeremy was remotely lecturing at Howard during the final year of his PhD teaching an introduction to computer science course. The professor position allows him to continue his teaching and research pursuits at his alma mater.

Congrats again Jeremy! I look forward to seeing all the mountains that you climb.