Building Better Systems

Latest Episodes:

#12: Alex Malozemoff & Marc Rosen – Censorship Circumvention with ROCKY Balboa Aug 12, 2021

Show notes

We chat with Alex Malozemoff and Marc Rosen about a recently published paper on a novel system for censorship circumvention, and it's corresponding implementation. The paper authors also include James Parker.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Alex Malozemoff: https://galois.com/team/alex-malozemoff/

Marc Rosen: https://galois.com/team/marc-rosen/

Paper referenced: Balboa: Bobbing and Weaving Around Network Censorship: https://arxiv.org/abs/2104.05871

#11: Alastair Reid – Meeting Developers Where They Are Jul 23, 2021

Show notes

Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Alastair Reid's paper project: https://alastairreid.github.io/RelatedWork/papers/

Rust verification tools: https://github.com/project-oak/rust-verification-tools

Meeting Developers Where They Are paper: https://arxiv.org/abs/2010.16345

Galois, Inc.: https://galois.com/

#10: Gregory Malecha – Formal Methods and Systems Programmers Working Together Jun 11, 2021

Show notes

Gregory Malecha talks with Joey and Shpat about Bedrock, a startup bringing systems engineers together with formal methods engineers to build some of the most secure and correct systems in the world.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Gregory Malecha: https://www.linkedin.com/in/gregory-malecha-91a71469/

https://gmalecha.github.io/

Formal Methods for the Informal Engineer: https://fmie2021.github.io/agenda.html

Galois, Inc.: https://galois.com/

#9: Tycho Andersen – Commit Log Spelunking May 13, 2021

Show notes

Tycho Andersen shares lessons that Linux kernel developers have learned from decades of open-source interactions. We discuss how the open-source community works together to make the Linux kernel better for everyone, and also what it's like to work debugging the kernel.

Watch all our episodes on the Building Better Systems Youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Tycho Andersen: https://tycho.pizza/

Galois, Inc.: https://galois.com/

#8: Eric Davis – Building Better Data Models Apr 15, 2021

Show notes

Dr. Eric Davis walks us through what it means for a data model to be trustworthy, what common pitfalls predictive models run into, reproducibility issues, and what can be done. We chat about how subject area experts are expected to be many things: statisticians, computer scientists, and mathematicians, and how that can sometimes lead to mistakes. We also look at the COVID-19 pandemic and how data models affect decision-making.

https://www.imagwiki.nibib.nih.gov/ https://www.imagwiki.nibib.nih.gov/content/committee-credible-practice-modeling-simulation-healthcare-description https://www.biorxiv.org/content/10.1101/2020.08.07.239855v1 https://www.imagwiki.nibib.nih.gov/content/10-simple-rules-conformance-rubric

You can watch this episode on our Youtube Channel: https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Eric Davis: https://galois.com/team/eric-davis/

Galois, Inc.: https://galois.com/

#7: Aditya Thakur – “If it goes too slow, they'll turn it off”: Analysis Tools That Work Apr 01, 2021

Show notes

Dr. Aditya Thakur, a computer science professor at U.C. Davis, walks us through his work on developing analysis tools that he wished he had while working in industry at places like Google. Aside from program analysis, we talk about making a research group successful by exposing them to industry. Towards the end, he shares his work on techniques and tools for repairing a trained deep neural network once a mistake has been discovered. Along the way, we learn about things like abstract interpretation, non-determinism, the trickiness of parallelism, and other concepts pertinent to analysis in an approachable way.

You can watch this episode on our Youtube Channel: https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Aditya Thakur: http://thakur.cs.ucdavis.edu/

Galois, Inc.: https://galois.com/

#6: Dan Guido – What the hell are the blockchain people doing, and why isn't it a dumpster fire? Feb 04, 2021

Show notes

Dan Guido, CEO of Trail of Bits, walks us through how they work with customers to make long-term improvements in security and software quality. He also describes what blockchain has done right, and how the rest of the software world should learn from them.

You can watch this episode on our Youtube Channel.

https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Dan Guido: https://www.linkedin.com/in/danguido/

Trail of Bits blog: https://blog.trailofbits.com/

Galois, Inc.: https://galois.com/

#5: Talia Ringer – Proof Engineering for the People Jan 11, 2021

Show notes

Talia Ringer, a Ph.D. candidate at University of Washington, explains how they do deep people-centric PL research. We discuss proof repair, UX for software correctness, and how to ask users of tools for feedback to react to.

You can watch this episode on our Youtube Channel.

Joey Dodds: https://galois.com/team/joey-dodds/

Talia Ringer: https://dependenttyp.es/

Galois, Inc.: https://galois.com/

#4: Alex Malozemoff – New attack on homomorphic encryption libraries: what does it mean? Dec 15, 2020

Show notes

Principal Researcher, Alex Malozemoff, walks us through what homomorphic encryption is, what CKKS is, and how a recent new attack on CKKS will impact progress on homomorphic encryption.

You can watch this episode on our Youtube channel.

Galois, Inc.

Joey Dodds

Shpat Morina

Alex Malozemoff

On the Security of Homomorphic Encryption on Approximate Numbers by Baiyu Li and Daniele Micciancio

#3: Stephen Magill & Tom DuBuisson – Musing on continuous code analysis Dec 03, 2020

Show notes

The founders of MuseDev discuss making modern static analysis usable and leveraging the latest promising research for automatic bug finding. MuseDev is a spin-off of Galois.

Video of this podcast can be found on our Youtube channel:

Galois, Inc.: https://galois.com/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Muse.dev

Tom Dubuisson: https://www.linkedin.com/in/thomas-dubuisson-62910453/

Stephen Magill, https://www.linkedin.com/in/stephen-magill-2070a096/

Continuous Reasoning: Scaling the impact of formal methods by Peter W. O’Hearn https://bit.ly/2I0TJEs