Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)

Abstract: My talk will present a distributed secure architecture for “cellularization,” a process in which utilities of the players are aligned by credible/non-credible threats. The proposed solution relies on a novel decentralized permissionless cyber-physical architecture that enables players to participate in Information-Asymmetric (Signaling) games, where deception is tamed by costly signaling, formal verification and zero-knowledge cryptography. The signaling, in order to remain honest (e.g., separating), may also involve asymmetric cryptography, crypto-tokens and distributed ledgers. Here, we will present a rough sketch of the architecture and the protocols it involves. Mathematical and computational analyses will appear in a companion paper.

Speaker: Professor Bud Mishra, Courant Institute

Bio: Professor Bud Mishra: An educator, an inventor as well as a mentor to technologists, entrepreneurs and scientists. Prof. Mishra founded the NYU/Courant Bioinformatics Group, a multi-disciplinary group working on research at the interface of computer science, applied mathematics, biology, biomedicine and bio/nano-technologies as well as Tandon-Online program on Bioinformatics Engineering.

Prof. Mishra has industrial experience in Computer and Data Science (aiNexusLab, ATTAP, behold.ai, brainiad, Genesis Media, Pypestream, and Tartan Laboratories), Finance (Instadat, Pattern Recognition Fund, Prospero.ai and Tudor Investment), Robotics and Bio- and Nanotechnologies (Abraxis, Bioarrays, InSilico, MRTech, OpGen and Seqster). He is the author of a textbook on algorithmic algebra and more than two hundred archived publications. He has advised and mentored more than 35 graduate students and post-docs in the areas of computer science, robotics and control engineering, applied mathematics, finance, biology and medicine.

He holds 23 issued and 21 pending patents in areas ranging over robotics, model checking, intrusion detection, cyber security, emergency response, disaster management, data analysis, biotechnology, nanotechnology, genome mapping and sequencing, mutation calling, cancer biology, fintech, adtech, internet architecture and linguistics.

Prof. Mishra’s pioneering work includes: first application of model checking to hardware verification; first robotics technologies for grasping, reactive grippers and work holding; first single molecule genotype/haplotype mapping technology (Optical Mapping); first analysis of copy number variants with a segmentation algorithm, first whole-genome haplotype assembly technology (SUTTA), first clinical-genomic variant/base calling technology (TotalRecaller), first single-molecule single cell nanomapping technology, first non-invasive liquid-biopsy technology, etc.

Prof. Mishra is currently a professor of computer science and mathematics at NYU’s Courant Institute of Mathematical Sciences, professor of engineering at NYUs Tandon School of engineering, professor of human genetics at MSSM Mt. Sinai School of Medicine, visiting scholar in quantitative biology at CSHL Cold Spring Harbor Laboratory and a professor of cell biology at NYU SoM School of Medicine. Prof. Mishra has a degree in Science from Utkal University, in Electronics and Communication Engineering from IIT, Kharagpur, and MS and PhD degrees in Computer Science from Carnegie-Mellon University. He is a fellow of IEEE, ACM, AAAS and EAI, a fellow of National Academy of Inventors (NAI), a Distinguished Alumnus of IIT (Kharagpur), and an NYSTAR Distinguished Professor.

Abstract: Formal verification has become a well-established part of standard hardware design flows leveraging SAT solvers and model checkers for verification tasks including logical equivalence checking, property checking, and protocol verification. These tools are largely based on all-digital, synchronous, single clock-domain models of hardware behaviour. To address the needs of system-on-chip and multi-core designs, we are developing verification methods for asynchronous, analog, mixed-signal, and mixed-timing circuits.

A key enabling technology for our research is the integration of an SMT solver, Z3, into an interactive theorem prover, ACL2. Our integration, Smtlink, exploits ACL2’s extensive support for reflection: we can write lisp functions that operate on the syntax of pending goals by extracting facts (e.g. function definitions and previously proven theorems) from the ACL2 logical world. Smtlink can automatically translate high-level goals that include user-defined data types and recursive functions into formulas that are in the logic of the SMT solver. We demonstrate the efficacy of this approach with the verification of timed asynchronous handshake circuits and a convergence proof for a digital phase-locked loop.

I will briefly describe related verification work including using automatic differentiation (AD) based algorithms to reason about synchronizers and analog circuits, and interval-arithmetic based verification algorithms to reason about convergence properties of non-linear circuits. Currently, I am working with students and other faculty at UBC to explore verification challenges arising in operating system research, cyber-physical systems, and numerical optimization algorithms used for machine learning.

I gratefully acknowledge my collaborators including Chris Chen, Ian Jones, Matt Kaufmann, Carl Kwan, Yan Peng, Justin Reiher, Mark Schmidt, and Margo Seltzer.

Bio: Mark Greenstreet is a professor in the Department of Computer Science at the University of British Columbia. He earned his B.Sc. (1981) from Caltech, and his MA (1988) and Ph.D. (1992) from Princeton. His research interests span a wide range of formal verification topics, especially any problem, hardware or software, that involves concurrency and/or continuous models. Mark has industrial chip design experience spanning from a design of an FFT chip set for ESL (at TRW subsidiary) in the early 1980’s to work on verifying the synchronizers and clock-domain-crossing circuits in many generations of SPARC CPUs.

Title:

Formally Verifying Implementations of Distributed Systems

Abstract:

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. In this talk, we'll survey the Verdi project which provides a framework for implementing and formally verifying implementations of distributed systems in Coq. Verdi eases the verification burden by enabling developers to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. Using this approach, the Verdi team produced the first correctness proof for an implementation of the Raft distributed consensus protocol.

Bio:

Zach Tatlock is an Assistant Professor in Computer Science and Engineering at the University of Washington where he leads the Programming Languages and Software Engineering (PLSE) group. He received his PhD from UC San Diego and BS from Purdue (where he took nearly every course with Bill Harris!). His research draws upon proof assistants, SMT solvers, and type systems to improve software reliability and security in domains ranging from distributed systems and compilers to web browsers. He can juggle and solve Rubik’s cubes, but not at the same time.

Abstract: Developer tools that support multiple languages generally have very limited regex-based code-analysis capabilities. Tree-sitter is a new parsing system that aims to change this paradigm. We’re in the process of integrating Tree-sitter into both GitHub.com and Atom, which will allow us to analyze code accurately and in real-time, paving the way for better syntax highlighting, code navigation, and refactoring support. We’ll demo some new features that Tree-sitter has enabled in GitHub.com and Atom, discuss its implementation, and share thoughts on ways it could be used in the future.

Bio: Max Brunsfeld is an engineer on GitHub’s Atom team. Prior to joining GitHub, he worked at Pivotal Labs as a full-stack engineer. He enjoys programming, especially in C and C++, jazz guitar, bicycling and hiking. He lives in Portland with his wife and two toddlers.