nsafoundry.blogg.se

In particular, his research focuses on designing programming languages, type systems, and other static analyses, that help programmers write provably secure and better performing software.📥 Read Formal Verification Report: Phase 1

His research interests broadly span the areas of programming languages, program verification, and security. of University of Maryland, College Park, advised by Michael Hicks.

Finally we extract the interpreter F* code to OCaml and provide a verified interpreter for running SMCs.Īseem Rastogi is a Ph.D. We also formalize the Wysteria interpreter in F*, and mechanize the proof of simulation theorem that relates the two semantics of Wysteria. The embedding enables programmers to use F*’s expressive logic to verify properties of their programs. al.) by defining a new monad and specifying the Wysteria type system checks as pre- and post-conditions of the API. Specifically, we embed Wysteria in F* (Nikhil Swamy et. In our current work, we validate that hypothesis and provide a framework for formally verifying the correctness and security properties of SMCs. We hypothesized that Wysteria makes it easy to analyze SMC programs, since the language provides an easy-to-understand single-threaded interpretation that corresponds to the actual multi-threaded semantics. Recently we designed a high-level functional programming language, called Wysteria, for writing SMCs. Applications of SMC include auction, private set intersection, statistical computation, and online games such as poker. In secure multi-party computation (SMC), mutually distrusting parties cooperatively compute functions of their private data in the process, they only learn certain results as per the protocol (e.g., the final output).