Molly: A Verified Compiler for Cryptoprotocol Roles

• URL: http://arxiv.org/abs/2311.13692v1
• Date: Wed, 22 Nov 2023 21:04:07 GMT
• Title: Molly: A Verified Compiler for Cryptoprotocol Roles
• Authors: Daniel J. Dougherty, Joshua D. Guttman,
• Abstract summary: Molly compiles cryptographic protocol roles into straight-line programs. We define a denotational semantics for protocol roles based on an axiomatization of the runtime.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Molly is a program that compiles cryptographic protocol roles written in a high-level notation into straight-line programs in an intermediate-level imperative language, suitable for implementation in a conventional programming language. We define a denotational semantics for protocol roles based on an axiomatization of the runtime. A notable feature of our approach is that we assume that encryption is randomized. Thus, at the runtime level we treat encryption as a relation rather than a function. Molly is written in Coq, and generates a machine-checked proof that the procedure it constructs is correct with respect to the runtime semantics. Using Coq's extraction mechanism, one can build an efficient functional program for compilation.

Related papers

• A Proof-Producing Compiler for Blockchain Applications [0.0873811641236639]
  CairoZero is a programming language for running decentralized applications (dApps) at scale. cryptographic protocols are used to verify the results of execution efficiently on blockchain. We show how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications.
  arXiv  Detail & Related papers  (2025-01-25T00:31:47Z)
• What can Large Language Models Capture about Code Functional Equivalence? [24.178831487657945]
  We introduce SeqCoBench, a benchmark for assessing how Code-LLMs can capture code functional equivalence. We conduct evaluations on state-of-the-art (Code)-LLMs to see if they can discern semantically equivalent or different pairs of programs in SeqCoBench.
  arXiv  Detail & Related papers  (2024-08-20T11:19:06Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• SparseCoder: Identifier-Aware Sparse Transformer for File-Level Code Summarization [51.67317895094664]
  This paper studies file-level code summarization, which can assist programmers in understanding and maintaining large source code projects. We propose SparseCoder, an identifier-aware sparse transformer for effectively handling long code sequences.
  arXiv  Detail & Related papers  (2024-01-26T09:23:27Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning. The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
  arXiv  Detail & Related papers  (2023-12-07T17:51:43Z)
• Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation [61.50286000143233]
  ChainCoder is a program synthesis language model that generates Python code progressively. A tailored transformer architecture is leveraged to jointly encode the natural language descriptions and syntactically aligned I/O data samples.
  arXiv  Detail & Related papers  (2023-04-28T01:47:09Z)
• A Formalization of Operads in Coq [0.0]
  In this paper, we discuss our formalization of an operad in the proof assistant Coq. Coq provides a formal mathematical basis for our meta-language development within V-SPELLS. Our work also provides, to our knowledge, the first known formalization of operads within a proof assistant that has significant automation.
  arXiv  Detail & Related papers  (2023-03-15T19:29:40Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  cryptography has been an exception, where many performance-critical routines have been written directly in assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce. On the formal-verification side, we connect to the FiatOpt framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker.
  arXiv  Detail & Related papers  (2022-11-19T11:07:39Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  Large language models (LLMs) produce code from informal natural language (NL) intent. It is hard to define a notion of correctness since natural language can be ambiguous and lacks a formal semantics. We describe a language-agnostic abstract algorithm and a concrete implementation TiCoder.
  arXiv  Detail & Related papers  (2022-08-11T17:41:08Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  Execution result--minimum Bayes risk decoding for program selection. We show that it improves the few-shot performance of pretrained code models on natural-language-to-code tasks.
  arXiv  Detail & Related papers  (2022-04-25T06:06:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.