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 appending zero-knowledge proofs (ZKPs) with system outputs that prove desired properties of the communicated data without revealing sensitive information. This approach allows us to give guarantees about the data that can then be used to ensure system integrity while maintaining confidentiality. This extends our trusted computing base well beyond our own system, allows us to reason about programs formally even without complete information, and grants us fine-grained control over which bits of information to keep secret. To demonstrate our capability, we created a prototype compiler to read type annotations from source files and generate ZKPs to enforce system compatibility.
Bio:
Dani Barrack is a Post Master’s student researcher in the Advanced Research in Cyber Systems group at Los Alamos National Laboratory. Her research focuses on novel applications of cryptographic zero-knowledge proofs, advanced type systems, and functional programming. She recently graduated from the Portland State University Computer Science program, where she completed a thesis under the supervision of Dr. Mark P. Jones on the use of a novel approach to verify compiler optimizations. Previously she had worked on a parallel computational physics backend at Los Alamos National Laboratory, on the verification group for medical device testing software at Microsystems Engineering Inc, and in the Basic Medical Sciences group at Western University of Health Sciences. She also holds a BS in Microbiology with minors in Japanese and Chemistry from Oregon State University.
Galois was pleased to host this tech talk via live-stream for the public. A video of the presentation can be found above.