Public Tech Talk: “hacspec – a specification language for crypto primitives and more” by Franziskus Kiefer

Monday, August 15, 2022

Abstract: An introduction and overview of hacspec, its design principles, and usage. Bio:   Franziskus is a security & cryptography engineer and researcher based in Berlin. He is co-founder of Cryspen, a company that builds custom high assurance cryptography. Franziskus holds a PhD in provable cryptography and was previously leading the security engineering efforts at Wire […]

Read More

Public Tech Talk: “Verifying the Ethics of Autonomous Systems” by Colin Shea-Blymyer

Monday, August 22, 2022

Abstract: Autonomous Intelligent Systems are often designed with complex, interacting objectives, or have learned behavior that is difficult to specify. This obfuscates the social and ethical rules of systems like self-driving vehicles and nursing robots in hospitals. Though their missions (e.g., go from point A to point B) are known, we need to determine their […]

Read More

Public Tech Talk: “Secure System Composition and Type Checking using Cryptographic Proofs” by Dani Barrack

Wednesday, July 20, 2022

Abstract: Formally verifying security properties and the functional correctness of systems involves comprehensive analyses of system compatibility and interoperability. Many conventional approaches require trusted systems in order to assure properties of transmitted data that are difficult to authenticate, or the undesirable exposure of additional data for the purpose of verification. We overcome this limitation by […]

Read More

Public Tech Talk: “Designing Data-Driven Yet Verifiably Safe Autonomous Medical Systems” by Taisa Kushner

Tuesday, July 12, 2022

Abstract: The exponential rise in data has spurred significant interest in developing personalized machine models for a seemingly infinite range of applications. However, in the case of safety critical systems such as autonomous medical systems, classical algorithms have failed due to complications spanning from limited data to the requirement that systems be explainable and verifiably […]

Read More

Public Tech Talk: “Expanding the Reach of Fuzzing” by Caroline Lemieux

Tuesday, April 19, 2022

Abstract: Software bugs are pervasive in modern software. As software is integrated into increasingly many aspects of our lives, these bugs have increasingly severe consequences, both from a security (e.g. Cloudbleed, Heartbleed, Shellshock) and cost standpoint. Fuzzing refers to a set of techniques that automatically find bug-triggering inputs by sending many random-looking inputs to the […]

Read More

Public Tech Talk: “Stealthy Attacks and Attack-Resilient Interval Estimators”

Tuesday, July 20, 2021

Abstract: Industrial control systems have been frequent targets of cyber attacks during the last decade. Adversaries can hinder the safe operation of these systems by tampering with their sensors and actuators, while ensuring that the monitoring systems are not able to detect such attacks in time. In this talk, we present methods to design and […]

Read More

Public Tech Talk: “Toward Robot Autonomy: Tasks, Plans, and Policies”

Friday, May 28, 2021

Abstract: Robots are increasingly deployed outside of carefully controlled factory settings. Advances in robot motion planning have made it possible to compute feasible motions for complex systems. My work is focused on increasing the abstraction level and time horizon of the types of robot tasks that (a) can be specified, (b) are computationally tractable, and […]

Read More

Public Tech Talk: “Gillian Verification of JavaScript and C”

Wednesday, May 05, 2021

Abstract: We will give a general introduction to Gillian, a platform for the development of symbolic-execution tools for many programming languages.  Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations […]

Read More

Public Tech Talk: “Refutation-based Adversarial Robustness Verification of Deep Neural Networks”

Friday, March 26, 2021

Abstract: Advances in deep neural networks (DNNs) have increased their deployment in safety-critical systems, such as vision perception modules for autonomous vehicles and airborne collision avoidance system controllers for unmanned aircraft. Modern DNNs and linear classifiers are susceptible to adversarial input perturbations. Adversarial perturbations are small changes to an input that result in unexpected changes […]

Read More

Public Tech Talk: “Toward Automatic Operating System Ports via Code Generation and Synthesis”

Friday, January 22, 2021

The slides for this presentation can be found here. Abstract: Porting operating systems is expensive; it costs time and money and (particularly) the attention of senior developers. Furthermore, with the end of Moore’s Law, portability is becoming more important again. Against this background, recent advances in program synthesis and the increasing availability of formal specifications for machine architectures offer an […]

Read More