C3E 2020 Discussion Series
July 31, 2020
John Backes (Amazon Web Services)
Automated reasoning in the cloud: How AWS is building services to help customers prove their security
John Backes is an AWS Senior Software Development Engineer. John will provide a presentation titled, “Automated reasoning in the cloud: How AWS is building services to help customers prove their security.”
August 14, 2020
Tyler Moore (University of Tulsa)
The Economic of Cybersecurity (linked to slides)
ABSTRACT: We often think of cybersecurity as a purely technical problem. However, cybersecurity failures are often better explained by economics rather than technology alone. In this talk, I describe how misaligned incentives and market failures can expose organizations to attacks despite spending record amounts on countermeasures. I will explore how firms typically manage their cybersecurity investment, review available policy interventions to correct market failures, and stake out open research questions for how lessons from security economics might be leveraged to improve the adoption of secure software development processes.
Tyler Moore is an Associate Professor of Computer Science at the University of Tulsa, where he holds the Tandy Chair of Cyber Security and Information Assurance. His research focuses on security economics, cybercrime measurement, and cybersecurity policy. He is a founding Editor in Chief of the Journal of Cybersecurity, a new interdisciplinary journal published by Oxford University Press. He was a 2016-17 New America Cybersecurity Fellow. Prior to joining TU, he was a postdoctoral fellow at the Center for Research on Computation and Society (CRCS) at Harvard University, the Hess Visiting Assistant Professor of Computer Science at Wellesley College, and an assistant professor at Southern Methodist University. A British Marshall Scholar, Prof. Moore completed his PhD at the University of Cambridge, while he holds BS degrees in Computer Science and Applied Mathematics from the University of Tulsa.
August 28, 2020
Fred B. Schneider
Metric or English: Characterizing and Conveying Trustworthiness
ABSTRACT: Not only do we seek trustworthy systems, but we must be convinced that trustworthiness is being achieved, and we must convince others of it too. We similarly seek a way to convey the returns from research in this space. Yet means of quantification have eluded us. This talk will survey the landscape, characterizing what we might expect of a characterization of trustworthiness (along with inherent limitations) and what kinds of vehicles are infeasible.
Fred B. Schneider is the Samuel B. Eckert Professor of Computer Science at Cornell, where he has been on the faculty since 1978. Schneider's research concerns trustworthy systems, most recently focusing on computer security.
September 11, 2020
Nikhil Swamy (Microsoft Research)
Programming with Proofs for High-assurance Software (linked to slides)
ABSTRACT: Programming critical systems with proofs, a long-standing goal of computer science, is beginning to come within reach of modern programming languages and proof assistants. I provide a brief overview of recent accomplishments in this space, related to work in the F* proof assistant and Project Everest, one of its flagship applications. Programs developed in F* with proofs of correctness are now deployed in wide variety of settings, ranging from Microsoft Windows and Hyper-V, Microsoft Azure, the Linux kernel, Firefox, mbedTLS, third party financial and trading software, and several others production systems. Rather than aiming to replace the full software stack, by carefully targeting the most security-critical components in existing high-value systems and replacing them with formally proven variants, we find that formal proofs can be adopted incrementally with tangible benefits to the security and reliability of the existing software stack.
Nikhil Swamy is a Senior Principal Researcher in the RiSE group at Microsoft Research, Redmond. His work covers various topics including type systems, program logics, functional programming, program verification and interactive theorem proving. He often thinks about how to use these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code. https://www.microsoft.com/en-us/research/people/nswamy/
September 25, 2020
Franjo Ivancic (Google)
Continuous Fuzzing at Google
ABSTRACT: At Google, tens of thousands of security and robustness bugs have been found by fuzzing C and C++ libraries. The various aspects of the SunDew project, one of the projects working on automated scalable techniques related to fuzzing at Google, are presented: how to fuzz, what to fuzz, and how to deal with discovered bugs. First, a distributed fuzzing infrastructure is presented. It allows to cooperatively utilize multiple test generation techniques. Then, a system for automated fuzz driver generation, named FUDGE, is described, which automatically generates fuzz driver candidates for libraries based on existing client code. Running large-scale fuzzing services also causes lots of bugs and vulnerabilities to be reported. Various techniques are presented to provide feedback to developers to reduce the time a known security bug remains open. Finally, challenges and opportunities to incorporate security testing into the general software development workflow are highlighted.
Franjo Ivancic is a Staff Software Engineer at Google in New York focusing on application security, program analysis and software development productivity tools. Prior to joining Google, he was a Senior Researcher at NEC Labs in the Systems Analysis and Verification group in Princeton, NJ. He received a Ph.D. in Computer and Information Science from the University of Pennsylvania in Philadelphia, PA, on modeling and verification of cyber-physical systems.
October 9, 2020
Gerard Holzmann (Nimble Research)
Interactive Code Analysis with Cobra
Gerard Holzmann is a 2015 Harlan D. Mills award winner as well as a Paris Kanellakis award winner. He is best known for the design and implementation of the popular logic model checking tool Spin. His software tool, Cobra, is a generic, fast and light-weight, static and dynamic analyzer.
October 23, 2020
Moshe Y. Vardi (Rice University)
Lessons from COVID-19: Efficiency vs Resilience (linked to slides)
ABSTRACT: In both computer science and economics, efficiency is a cherished property. In computer science, the field of algorithms is almost solely focused on their efficiency. In economics, the main advantage of the free market is that it promises "economic efficiency". A major lesson from COVID-19 is that both fields have over-emphasized efficiency and under-emphasized resilience. I argue that resilience is a more important property than efficiency and discuss how the two fields can broaden their focus to make resilience a primary consideration. I will include a technical example, showing how we can shift the focus in strategic reasoning from efficiency to resilience.
Moshe Y. Vardi is University Professor and the George Distinguished Service Professor in Computational Engineering at Rice University. He is the recipient of several awards, including the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, and the EATCS Distinguished Achievements Award. He is the author and co-author of over 650 papers, as well as two books. He is a fellow of several societies, and a member of several academies, including the US National Academy of Engineering and National Academy of Science. He holds seven honorary doctorates. He is a Senior Editor of the Communications of the ACM, the premier publication in computing.
November 6, 2020
Series Summary and Wrap-up
Speakers:
Patrick Lincoln (SRI International)
Warren A. Hunt, Jr. (UT Austin)
Carl Landwehr (Independent Consultant)
Stephen Magill (Muse Dev)
Fred B. Schneider (Cornell University)
Rance Cleaveland (National Science Foundation)
John C. Mallery (MIT CSAIL)
Patrick Lincoln is Vice President of Information and Computing Sciences, and director of the Computer Science Laboratory (CSL) at SRI International. Lincoln leads research in the fields of formal methods, computer security and privacy, computational biology, scalable distributed systems, and collaborative interfaces.
Warren A. Hunt, Jr. is Professor in the Department of Computer Sciences of the University of Texas at Austin. Dr. Hunt holds a BSEE from Rice University and a PhD in computer science from the University of Texas. His research interests include hardware verification, circuit design, SAT solving, and mechanized theorem proving.
Carl E. Landwehr is Fellow of the IEEE and a member of the first class of inductees to the National Cybersecurity Hall of Fame. His research focus is cybersecurity and trustworthy computing. His work has addressed the identification of software vulnerabilities toward high assurance software development, architectures for intrusion-tolerant and multilevel security systems, token-based authentication, and system evaluation and certification methods. His thirty-five year career in cybersecurity R&D includes service with the Naval Research Laboratory, National Science Foundation, IARPA, and several other institutions.
Stephen Magill has spent over 15 years advancing the state of software security and privacy via both basic research and technology transition efforts. Stephen currently serves as CEO of Muse Dev, a company focused on bringing advanced static analysis and verification capabilities to developers.
Fred B. Schneider is Samuel B. Eckert Professor of Computer Science at Cornell University. He joined Cornell's faculty in Fall 1978 and served as department chair from 2014 through 2018, having completed a Ph.D. at Stony Brook University and a B.S. in Engineering at Cornell in 1975. Schneider's research has focused on various aspects of trustworthy systems --- systems that will perform as expected, despite failures and attacks.
Rance Cleaveland is Professor of Computer Science at the University of Maryland (UMD) at College Park. Since 2018, he has also been serving as Division Director of the Computing and Communication Foundations (CCF) division within the Computer and Information Science and Engineering (CISE) directorate of the National Science Foundation. He has published over 140 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, verification tools, software testing, and software architecture
John C. Mallery is a research scientist at the MIT Computer Science & Artificial Intelligence Laboratory. He is concerned with cyber policy and has been developing advanced architectural concepts for cyber security and transformational computing for the past decade. Since 2006, he organized a series of national workshops on technical and policy aspects of cyber.