English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Secure multi-party computation (MPC) enables a set of mutually distrustingparties to cooperatively compute, using a cryptographic protocol, a functionover their private data. This paper presents Wys*, a new domain-specificlanguage (DSL) for writing mixed-mode MPCs. Wys* is an embedded DSL hosted inF*, a verification-oriented, effectful programming language. Wys* sourceprograms are essentially F* programs written in a custom MPC effect, meaningthat the programmers can use F*'s logic to verify the correctness and securityproperties of their programs. To reason about the distributed runtime semanticsof these programs, we formalize a deep embedding of Wys*, also in F*. Wemechanize the necessary metatheory to prove that the properties verified forthe Wys* source programs carry over to the distributed, multi-party semantics.Finally, we use F*'s extraction to extract an interpreter that we have provedmatches this semantics, yielding a partially verified implementation. Wys* isthe first DSL to enable formal verification of MPC programs. We haveimplemented several MPC protocols in Wys*, including private set intersection,joint median, and an MPC card dealing application, and have verified theircorrectness and security.

WYS*: A DSL for Verified Secure Multi-party Computations