December 2020 involved a couple of major events related to our hardware security research — a HOST Tutorial and a CASA Distinguished Lecture. Ryan and Dr. Nicole Fern from Tortuga Logic gave a tutorial at IEEE International Symposium on Hardware Oriented Security and Trust (HOST) HOST 2020. Ryan was also invited to give a Distinguished Lecture in the CASA Cluster of Excellence at Ruhr University Bochum. Both events focused on our work on Property Driven Hardware Security.

Property driven hardware security is a design methodology to assess the safety and security of hardware designs. It enables security experts to describe how the hardware should (or should not) function. These security properties are formally specified using languages that map to models that are easy to verify using existing design tools. There are three fundamental elements for any hardware security design flow. First, security experts need expressive languages to specify these security properties. Second, these properties should map to models to describe the security related behavior of a hardware design. Finally, hardware security design tools verify that the hardware design meets these properties using formal solvers, simulation, and emulation.

The HOST tutorial was one of six selected to provide HOST attendees with an in-depth look at important topics in hardware security. I gave a similar tutorial in the last HOST that was well-received and invited back for another year. This time around, the tutorial included Dr. Nicole Fern from Tortuga Logic. Nicole provided a great presentation on the types of properties that modern hardware security verification tools can handle. I added an in-depth look about how these tools can verify security properties. Have a look yourself at the materials made available to the attendees if you would like.

The Distinguished Lecture was a great honor for me. I really admire the research done in CASA Cluster of Excellence — they have an outstanding group of researchers that I have followed for many years (even decades). This invitation did lead me to consider what one needs to do in order to be eligible to give a distinguished lecture. My conclusion is that one mostly just needs to be a researcher for a long enough time and then their work becomes distinguished. And that made me feel a bit old. So before my talk I made sure to shave and pluck out grey hairs. The folks at CASA did a nice job of producing a video of the talk:

Liver cancer has the fastest growth of incidence and the second highest mortality of all cancers in the United States. Worldwide, it is estimated that over one million people will die from liver cancer in 2030. Liver resection (hepatectomy) is the paradigm for treating liver cancer. A crucial part of a partial hepatectomy is understanding where the tumors, vessels, and other important landmarks are located. To aid in this, the patient typically undergoes preoperative cross-sectional imaging (e.g., CT/MR scans). Surgeons use these images to determine resectability based upon the location of important structures (e.g., veins), analyze tumor margins, accurately compute future liver remnant volumes, and generally aid in surgical planning and navigation.

However, it is challenging for the surgeon to mentally register preoperative cross-sectional images to the surface of the liver at the time of operation since surgical actions cause significant and sometimes permanent liver deformations that lead to mismatches with cross-sectional images. Mentally integrating preoperative data into the operative field is time consuming and error prone. This can make it difficult to accurately localize smaller tumors intra-operatively, which can affect surgical decision making and adequate resection of primary and metastatic liver tumors.

Dr. Michael Barrow‘s PhD thesis developed augmented Reality (AR) image guidance techniques that merge preoperative data directly into the surgeons view during surgery. The goal is to provide surgeons with what Michael describes as “X-ray vision” — allowing them to see through tissues and better understand where blood vessels, tumors, and other important surgical landmarks lie.

The research brings together many state-of-the-art technologies. It requires computer vision approaches to track the surgical scene, real-time mechanical modeling of the organ to accurately place the important unseen surgical landmarks, augmented reality to visualize the landmarks, and hardware accelerated compute systems to process the high throughput sensor data. He showed that patient specific biomechanical modeling results in clinically significant increases in accuracy. Specifically, he built a system that uses magnetic resonance elastography to create a patient-specific mechanical model. The system works in real-time to provide accurate positions of unknown landmarks. He physically validated the techniques by creating a phantom mechanical platform to demonstrate it is possible to track landmarks internal to the phantom liver.

Michael took an unconventional path to his PhD. Unlike most PhDs, he laid out his research topic almost solely on his own. He spent a lot of time shadowing medical doctors to understand their problems. He deftly maneuvered through many different fields, seeking out and finding key collaborators. The result is an amazing example of an interdisciplinary thesis that has tremendous potential value in a clinical setting.

Michael developed a number of other technologies that are not reflected in his thesis. Most recently he is focusing on developing technologies to help into COVID-19 crisis which was awarded an UCSD Institute of Engineering in Medicine Galvanizing Engineering in Medicine award. He lead a team of undergraduates to build systems to better scale the care of COVID-19 patients (for more information see CSE Research Highlight).

Michael was a real tour de force in pushing collaborations between the School of Engineering and the School of Medicine. In addition to his Phd thesis project, he developed a close collaboration with Dr. Shanglei Liu and made many other connections between our research group and the medical school that will certainly create more future fruitful collaborations.

After graduation, Michael started a post-doctoral position at Lawrence Livermore National Labs.

Our large-scale 3D modeling work was featured on the National Geographic Docuseries “Ancient China from Above“. We developed 3D models using drones, multispectral cameras, lidar, and other cutting edge technology, which provided archaeologist Alan Maca new insights to better understand ancient Chinese civilizations.

As part of the production, Ryan and Eric Lo traveled to some of the most remote parts of China including Xanadu (Kublai Khan’s summer palace in Inner Mongolia), the Han Great Wall in the Gobi Desert, and Shimao — a new archaeological site known as China’s Pompeii located on the Loess plateau.

The three part series aired on the National Geographic Channel and is available on most video streaming platforms. The full “Secrets of the Great Wall” episode is available on YouTube. We appear around the 26 minute mark.

Hardware security-related attacks are growing in number and their severity. Spectre, Meltdown, Foreshadow, Fallout, ZombieLoad, and Starbleed are just a few of the many recent attacks that exploit hardware vulnerabilities. While vulnerabilities are seemingly easy to find, designing secure hardware is challenging (to say the least) and there are limited tools to aid this process.

Armita Ardeshiricham’s PhD thesis made pioneering and fundamental contributions in detecting, localizing, and repairing hardware vulnerabilities. Her thesis developed verification tools that quickly finds vulnerabilities that previous work could not. And it laid the foundation for automated debugging of those flaws.

Her early work focused on developing powerful information flow tracking (IFT) tools that that work at the register transfer level. She extended this work in a fundamentally important manner by formulating IFT logic that detects timing based flows. And she pioneered the idea of sketching for hardware security. The culmination of her PhD research is the VeriSketch framework.

VeriSketch is the first design framework that uses sketching to automatically synthesize secure and functionally-complete hardware design. VeriSketch frees hardware designers from specifying exact cycle-by-cycle behaviors and excruciating bit-level details that often lead to security vulnerabilities. Instead, the designer provides a sketch of the circuit alongside a set of functional and security properties. VeriSketch uses program synthesis techniques to automatically generate a fully-specified design which satisfies these properties. VeriSketch leverages hardware IFT to enable definition and verification of security specifications, which allows for the analysis of a wide variety of security properties related to confidentiality, integrity, and availability.

Armita’s PhD research will undoubtedly have a lasting impact on our group’s hardware security efforts and has laid out a research agenda for the next few years (and likely beyond). Based on her work, we have started projects on error localization (with Prof. Yanjing Li at Univ. of Chicago) and automated property generation (with Prof. Cynthia Sturton at Univ. of North Carolina) that was recently funded by the Semiconductor Research Corporation. Her work was fundamental in developing system on chip access control monitors in collaboration with Leidos and Sant’Anna School of Advanced Studies in Pisa. She will certainly be missed!

Dr. Ardeshiricham currently works at Apple doing things that she can tell no one about (as is typically with Apple). But I’m certain that future Apple devices will be much more secure with her overseeing the verification process.

A very long overdue post and congrats again!

-Ryan

Did you know that mangroves sequester more carbon than rainforests? In addition to being one of the best carbon scrubbers in the world, they also protect coastlines from erosion and hurricanes and provide an amazing nursery for aquatic life. Yet, these important ecosystems are in-decline worldwide, hurt by industrialization, rising sea levels, and other climatic events.

As part of the activities around World Mangrove Day, Ryan moderated an online panel “The Science Behind Remote Sensing” related to using technology to monitor and rehabilitate mangroves. The panel featured researchers from NASA, Microsoft, UCSD, and the Nature Conservancy are using drones, satellites, multispectral imaging, machine learning, and a bunch of other technologies to understand and rehabilitate mangroves around the world. Our collaborator Astrid Hsu presented some of the technologies that we are working on as part of Engineers for Exploration program. And there was a lot of interesting discussion on how to use technology to monitor, understand, and rehabilitate these important ecosystems.

Digitally documenting archaeological sites provides high-resolution 3D models that are more accurate than traditional analog (manual) recordings. Capturing the 3D data comes at great financial cost (if using a lidar-based system) or be time-consuming during data collection and post-processing (when using photogrammetry). This has limited the use of these techniques in the field.

Depth sensors like the Microsoft Kinect and Intel RealSense provide relative low-cost way of capturing depth data. Open-source 3D mapping software provides fast and accurate algorithms to turn this depth data into 3D models. Our research combines depth sensors and 3D mapping algorithms to develop a low-cost 3D scanning system. We analyzed multiple sensors and software packages to develop a prototype system to create large scale 3D model of tunneling-based archaeological site. We used this system to document Maya archaeological site El Zotz in the Peten region of Guatemala. Our findings were recently published in the paper “Low-cost 3D scanning systems for cultural heritage documentation” in the Journal of Cultural Heritage Management and Sustainable Development.

This research is the result of a many year (and on-going) effort between Engineers for Exploration and archaeologists at El Zotz. Congrats to all those involved in this impressive project.

Advanced wireless communication techniques, like those found in 5G and beyond, require low latency while operating on high throughput streams of radio frequency (RF) data. Automatic Modulation Classification is one important method to understand how other radios are using the wireless channel. This information can be used in applications such as cognitive radios to better utilize the wireless channel and transmit information at faster rates.

Our recent work shows how to perform modulation classification in real-time by exploiting the RF capabilities offered by Xilinx RFSoC platforms. This work, lead by the University of Sydney Computer Engineering Lab, developed a non-uniform and layer-wise quantization technique to shrink the large memory footprint of neural networks to fit on the FPGA fabric. This technique preserves the classification accuracy in a real-time implementation.
This work was published at the Reconfigurable Architectures Workshop (RAW) and an open source implementation on Xilinx RFSoC ZCU111 development board is available at in the github repo.

The Edward Alexander Bouchet Graduate Honor Society is a network of preeminent scholars who exemplify academic and personal excellence, foster environments of support, and serve as examples of scholarship, leadership, character, service, and advocacy for students who have been traditionally underrepresented in the academy. 

Jeremy will fit in perfectly. His research on hardware security is exploring new ways to mitigate side channel attacks. It has resulted in several research papers in top venues. His leadership, service, and advocacy are evident during his time as an undergraduate at Howard University and throughout his PhD career at UCSD. A small sampling of this includes tutoring and mentoring elementary, high school, and undergraduate students, many of which have come from underrepresented groups. He served as President of Jacob’s Graduate Student Council where he helped organize events for engineering students to present their research with their peers to get feedback for future presentations and to young students to inspire them to pursue engineering.

Edward Bouchet was the first African American doctoral recipient in the United States. He entered Yale College (now Yale University) in 1870. He graduated in 1874 and decided to stay on a couple more years to get his PhD in Physics. Despite an impressive academic record (he got a PhD in two years!), he was unable to land a position in a college or university due to his race. He taught chemistry and physics at the School for Colored Youth in Philadelphia for more than 25 years; it was one of the few institutions that offered African Americans a rigorous academic program. 

Our research was represented prominently at the CSE Research Open House, held on January 31, 2020. The open house provides an opportunity for industry, alumni, and broader UCSD community to get a view of the research going on in our department. It consisted of research talks in the morning, demos in the afternoon, a research poster session, and awards ceremony.

Engineers for Exploration (E4E) described their latest and greatest technologies during the sustainable computing session in the morning and showed off demos in the afternoon. The featured E4E projects included our project to document Maya archaeology sites where we use state of the art imaging sensors to create large scale 3D models of archaeological site. This is then viewable in virtual reality. Another featured project is mangrove monitoring which uses drones, multispectral image sensors, machine learning for automated ecosystem classification, and other new technologies to document and understand these fragile and important ecosystems. The radio collar tracker was the final presented project. The goal is to track animals equipped with radio transmitters using drones and software defined radio. Here’s the presentation if you want more detail on these projects and the E4E program.

Michael Barrow was awarded the best poster for his research on “Data Driven Tissue Models for Surgical Image Guidance“. Michael leads this multidisciplinary project that spans across the Jacobs School of Engineering and the School of Medicine. The goal is to develop more accurate modeling and visualization of tumors, blood vessels, and other important landmarks to provide surgeons real-time feedback during the operation.

Finally, our close collaborator Tim Sherwood was honored with a CSE Distinguished Alumni awards. We have been working with Tim for almost two decades (pretty much since the time he graduated from UCSD) Our research includes a number of fundamental projects in hardware security including some of the initial work in FPGA security, 3D integrated circuit security, hardware information flow tracking, and computational blinking.

While it took much, much longer than it should have, the semiconductor industry is starting to realize that security is a critical part of the design process. Spector, Meltdown, and other high profile hardware security flaws have shown the danger of ignoring security during the design and verification process. Intel, Xilinx, Qualcomm, Broadcom, NXP and other large semiconductor companies have large and growing security teams that perform audits for their chips to help find and then mitigate security flaws.

Emerging hardware security verification tools (including those spun out of our research group from Tortuga Logic) help find potential security flaws. They are powerful at detecting flaws that violate specified security properties and providing example behaviors on how to exploit the flaw. Unfortunately, fixing these flaws remains a manual process, which is time consuming and often left without a viable solution.

VeriSketch takes a first step at automatically fixing the bugs found by the hardware verification tools. VeriSketch asks the designer to partially specify the hardware design, and then uses formal techniques to automatically fill in the sketch to create a design that is guaranteed to be devoid of the flaw. It leverages program synthesis, which automatically constructs programs that fit given specifications. VeriSketch introduces program synthesis into the hardware design world and uses security and functional constraints for the specification. This allows hardware designers to leave out details related to the control (e.g., partially constructed finite state machines) and datapath (e.g., incomplete logic constructs). VeriSketch uses formal methods to automatically derive these unknown parts of the hardware such that they meet the security constraints.

As a proof of concept, we used hardware security verification tools to show that PLCache (a well known cache that is supposedly resilient to cache side channel) does indeed have a flaw through its meta-data (more specifically the LRU bit). And we were able to use VeriSketch to automatically augment the PLCache design to remove this flaw.

More details on VeriSketch, the PLCache flaw, and other interesting hardware security verification techniques are detailed in our paper “VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow Properties” presented at the ACM Conference on Computer and Communications Security. Congrats to the authors Armaiti Ardeshiricham, Yoshiki Takashima, Sicun Gao, and Ryan Kastner!