Computer systems are increasingly handling important information and responsible for controlling and protecting critical infrastructures; insuring that they behave in a secure manner is of the utmost importance. Information flow tracking is an important technique for determining the security of a computing system. It works by “labeling” important data and then automatically determining how it will move throughout the microelectronic circuit. This can be used to verify that the hardware and software are behaving in a correct manner, and eliminate costly security flaws.
We have been working on hardware information flow tracking for almost a decade, and we now finally decided it is time to increase the level of abstraction from gate level to register transfer level. Our recent paper at Design, Automation and Test in Europe (DATE) — the premier conference for electronic system design and test — detailed the benefits this approach by showing that formal verification can be made substantially faster, and we can more easily provide tradeoffs between complexity (i.e., verification time) and accuracy. This allows us verify the security of larger circuits which is important as security rightfully becomes a more prevalent consider in the hardware design flow.
The paper “Register Transfer Level Information Flow Tracking for Provably Secure Hardware Design” was authored by Armaiti Ardeshiricham, Wei Hu, Joshua Marxen and Ryan Kastner. Ryan returned to Lausanne, Switzerland to give the talk. It was a beautiful week as evidenced by the picture taken in vineyards in nearby Epesses above Lake Geneva.
Our work on localizing small underwater robots was recently published in Nature Communications. The article describes a swarm of little underwater robots, called Mini-Autonomous Underwater Explorers (M-AUE), that can change their depth, but otherwise drift along with currents. These robots were developed in Dr. Jules Jaffe’s Laboratory for Underwater Vision. While they seem very simple, this is allows for experimentation on how ocean currents effect different types of ocean phenomenon. In particular, a swarm of these robots were used to verify, for the first time, the physical–biological interaction leading to plankton patch formation in internal waves. Our role in the project was to determine where each of these drifter moves over the course of the experiment. Typically you can rely on GPS, but that unfortunately does not work underwater. We set up our own version of GPS, using buoys instead of satellites, and acoustic signals instead of radio signals. This complicate things substantially as acoustic signal are very messy when transmitted underwater. Nevertheless, we were able to develop tracking and localization algorithms that played a key role in uncovering these scientific findings.
Technical Paper: A swarm of autonomous miniature underwater robot drifters for exploring submesoscale ocean dynamics, Jules S. Jaffe, Peter J. S. Franks, Paul L. D. Roberts, Diba Mirza, Curt Schurgers, Ryan Kastner & Adrien Boch, Nature Communications 8, Article number: 14189 (2017)
Media coverage: LA Times, KPBS, Phys.org, Live Science, Cosmos, Extreme Tech, New Atlas, Digital Trends.
Ryan’s childhood dream has come true – speaking at MTV! Well, not exactly as it isn’t that MTV rather the Microprocessor Test and Verification Conference. But it was still an honor to give an invited talk at this conference in December. Our paper “Towards Property Driven Hardware Security” covers some of our group’s most recent security work and gives a glimpse at some future research directions. The paper defines a paradigm for a hardware security design flow that is focused on specifying important security properties early in the design process, and then using tools to test and verify that these properties hold during the entire design process. This work highlights some of the research efforts by Wei, Alric, and Armita. And given that MTV has moved far away from the good ole’ days of playing music videos (and now mostly plays mind numbing reality TV shows seemingly aimed at those with limited intelligence) this is probably a lot more prestigious. We miss you Matt Pinfield!
FPGAs are notoriously hard to use largely due to the lack of programming infrastructure. Recent synthesis tools that compile OpenCL code directly to an FPGA platform are attempting to reduce this programming burden. As part of our research in this domain, we developed the Spector benchmarks. These provide a number of different applications with tunable “knobs” that can be used to change the resource usage and performance. Furthermore, we have fully compiled each of these benchmarks with different knob setting and reported the results. The benchmarks are available in a repo under an open-source license. See our FPT paper for more information. And congrats to the authors Quentin, Alric, Pingfan, and Ryan.
Links: Spector paper, Spector repo
It would seem like one would want a “precise” solution to security, but our recently published work shows that this isn’t always the best. In particular, by reducing the complexity of the security model, you can allow the formal solvers to finish more quickly, and in many cases give you an answer where previously you wouldn’t get one at all. The latter case happens often — the tools never fail to give an answer because you are asking them too difficult a question; they can spend days or even weeks and still not be able to determine a result. Our recent publication at the International Conference On Computer Aided Design (ICCAD) demonstrates some techniques to take advantage of this complexity vs. precision tradeoff in order to analyze hardware design for security flaws. This work was co-authored with collaborators from EPFL (Andrew Becker and Paolo Ienne), and NPU (Dejun Mu), in addition to Kastner Research Group members, Wei, Armita, and Ryan.
Antonella traveled to Shanghai to present our paper “Autonomous Acoustic Trigger for Distributed Underwater Monitoring Systems” at WUWNet ’16: The 11th ACM International Conference on Underwater Networks and Systems. The paper, authored by Antonella, Ryan, and visiting undergraduates Ethan Slattery (University of California, Santa Cruz) and Andrew Hostler (California Polytechnic San Luis Obispo) earned 1st runner up for the Best Paper Award. The paper described the development of an autonomous underwater camera system for marine population monitoring, which has been used to autonomously monitor the vaquita porpoise in Mexico, and will be used in the coming months to study the Nassau grouper in the Cayman Islands and the kelp forest soundscape in San Diego.
Paper: “Autonomous Acoustic Trigger for Distributed Underwater Visual Monitoring Systems“
For the past couple of years, we have been participating in the Early Research Scholars Program (ERSP). This provides first or second year undergraduates a glimpse into the life of academic research. The goal is to allow the undergraduates to begin to understand what it means to be a researcher, write papers, deal with their annoying advisors, sit in on generally boring research group meetings, and experience all of the other activities of a university research group. It is a valuable and rewarding program run by Prof. Christine Alvarado and sponsored by the National Science Foundation. The second ERSP cohort sent our group a “thank you” card of sorts. It was very much appreciated. We certainly enjoyed working with those ERSP’ers (Proud Heng, Aishika Kumar, Rene Sanchez), and we look forward to seeing them go on to do great things. Of course, we hope that they will continue to do research with us. We would be honored to continue to have them as part of our research group.
Links: Early Research Scholars Program
Our group was well represented at the Oceans conference this year. Antonella Wilby and Riley Yeakle traveled to Monterey, CA to present two papers. The first paper discussed the development of an acoustic triggering system for an underwater camera trap. Antonella was the first author along Engineer for Exploration summer students Ethan Slattery (an undergraduate at UC Santa Cruz), Andrew Hostler (undergraduate at Cal Poly SLO), and Ryan. Riley presented work that details how one can use ambient acoustic ocean noise to determine the relative locations of underwater vehicles. This was joint work with Perry Naughton, Curt Schurgers, and Ryan. Of course, no visit to Monterey would be complete without a visit to the aquarium.
Links: “Design of a Low-Cost and Extensible Acoustically-Triggered Camera System for Marine Population Monitoring“, “Inter-node Distance Estimation from Ambient Acoustic Noise in Mobile Underwater Sensor Arrays“
Another Summer is gone and Fall Quarter and the new academic year is upon us. But before classes started up and campus awakened from its summer slumber, we spent a few days in Mammoth Lakes relaxing, hiking, kayaking, climbing, eating, drinking, and giving some research talks. Some of the highlights this year included homemade group dinners every night, an “easy” (compared to last year) group hike in Yosemite, and of course the compelling research discussions. Some pictures from our expert photographers (Quentin, Mike, Lu, and Ryan) are below.
The Office of Naval Research held a workshop aimed to identify key research areas for offensive of defensive hardware security research, metrics to measure high assurance, and approaches to mitigate threats. And ideally these are all deployable in the short term without modifications to the hardware. This is a tall task for sure. Ryan presented our group’s research on hardware security design tools including security testing and verification, metrics based upon information theoretic measures, and the need to employ application driven research. The workshop was hosted by Simha Sethumadhavan at Columbia University. The requisite foot picture of Columbia’s campus to prove that I was there.