-
Joint Alignment of Multivariate Quasi-Periodic Functional Data Using Deep Learning
Authors:
Vi Thanh Pham,
Jonas Bille Nielsen,
Klaus Fuglsang Kofoed,
Jørgen Tobias Kühl,
Andreas Kryger Jensen
Abstract:
The joint alignment of multivariate functional data plays an important role in various fields such as signal processing, neuroscience and medicine, including the statistical analysis of data from wearable devices. Traditional methods often ignore the phase variability and instead focus on the variability in the observed amplitude. We present a novel method for joint alignment of multivariate quasi…
▽ More
The joint alignment of multivariate functional data plays an important role in various fields such as signal processing, neuroscience and medicine, including the statistical analysis of data from wearable devices. Traditional methods often ignore the phase variability and instead focus on the variability in the observed amplitude. We present a novel method for joint alignment of multivariate quasi-periodic functions using deep neural networks, decomposing, but retaining all the information in the data by preserving both phase and amplitude variability. Our proposed neural network uses a special activation of the output that builds on the unit simplex transformation, and we utilize a loss function based on the Fisher-Rao metric to train our model. Furthermore, our method is unsupervised and can provide an optimal common template function as well as subject-specific templates. We demonstrate our method on two simulated datasets and one real example, comprising data from 12-lead 10s electrocardiogram recordings.
△ Less
Submitted 14 November, 2023;
originally announced December 2023.
-
Extracting functional programs from Coq, in Coq
Authors:
Danil Annenkov,
Mikkel Milo,
Jakob Botsch Nielsen,
Bas Spitters
Abstract:
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with ty** information and use it as an intermediate representation, which we call $λ^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented…
▽ More
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with ty** information and use it as an intermediate representation, which we call $λ^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised $λ^T_\square$ representation, we obtain code in two functional smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
△ Less
Submitted 6 August, 2021;
originally announced August 2021.
-
Extracting Smart Contracts Tested and Verified in Coq
Authors:
Danil Annenkov,
Mikkel Milo,
Jakob Botsch Nielsen,
Bas Spitters
Abstract:
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language E…
▽ More
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
△ Less
Submitted 26 April, 2021; v1 submitted 16 December, 2020;
originally announced December 2020.
-
Smart Contract Interactions in Coq
Authors:
Jakob Botsch Nielsen,
Bas Spitters
Abstract:
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq's functional language Gallina, enabling easier reason…
▽ More
We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq's functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress's behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.
△ Less
Submitted 12 November, 2019;
originally announced November 2019.
-
ConCert: A Smart Contract Certification Framework in Coq
Authors:
Danil Annenkov,
Jakob Botsch Nielsen,
Bas Spitters
Abstract:
We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we dev…
▽ More
We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.
△ Less
Submitted 20 December, 2019; v1 submitted 24 July, 2019;
originally announced July 2019.
-
Lower Bounds for Oblivious Data Structures
Authors:
Riko Jacob,
Kasper Green Larsen,
Jesper Buus Nielsen
Abstract:
An oblivious data structure is a data structure where the memory access patterns reveals no information about the operations performed on it. Such data structures were introduced by Wang et al. [ACM SIGSAC'14] and are intended for situations where one wishes to store the data structure at an untrusted server. One way to obtain an oblivious data structure is simply to run a classic data structure o…
▽ More
An oblivious data structure is a data structure where the memory access patterns reveals no information about the operations performed on it. Such data structures were introduced by Wang et al. [ACM SIGSAC'14] and are intended for situations where one wishes to store the data structure at an untrusted server. One way to obtain an oblivious data structure is simply to run a classic data structure on an oblivious RAM (ORAM). Until very recently, this resulted in an overhead of $ω(\lg n)$ for the most natural setting of parameters. Moreover, a recent lower bound for ORAMs by Larsen and Nielsen [CRYPTO'18] show that they always incur an overhead of at least $Ω(\lg n)$ if used in a black box manner. To circumvent the $ω(\lg n)$ overhead, researchers have instead studied classic data structure problems more directly and have obtained efficient solutions for many such problems such as stacks, queues, deques, priority queues and search trees. However, none of these data structures process operations faster than $Θ(\lg n)$, leaving open the question of whether even faster solutions exist. In this paper, we rule out this possibility by proving $Ω(\lg n)$ lower bounds for oblivious stacks, queues, deques, priority queues and search trees.
△ Less
Submitted 24 October, 2018;
originally announced October 2018.
-
Distributed Co-Simulation of Maritime Systems and Operations
Authors:
Severin Sad**a,
Lars T. Kyllingstad,
Martin Rindarøy,
Stian Skjong,
Vilmar Æsøy,
Dariusz Eirik Fathi,
Vahid Hassani,
Trond Johnsen,
Jørgen Bremnes Nielsen,
Eilif Pedersen
Abstract:
Here, we present the concept of an open virtual prototy** framework for maritime systems and operations that enables its users to develop re-usable component or subsystem models, and combine them in full-system simulations for prototy**, verification, training, and performance studies. This framework consists of a set of guidelines for model coupling, high-level and low-level coupling interfac…
▽ More
Here, we present the concept of an open virtual prototy** framework for maritime systems and operations that enables its users to develop re-usable component or subsystem models, and combine them in full-system simulations for prototy**, verification, training, and performance studies. This framework consists of a set of guidelines for model coupling, high-level and low-level coupling interfaces to guarantee interoperability, a full-system simulation software, and example models and demonstrators. We discuss the requirements for such a framework, address the challenges and the possibilities in fulfilling them, and aim to give a list of best practices for modular and efficient virtual prototy** and full-system simulation. The context of our work is within maritime systems and operations, but the issues and solutions we present here are general enough to be of interest to a much broader audience, both industrial and scientific.
△ Less
Submitted 4 January, 2017;
originally announced January 2017.
-
A New Approach to Practical Active-Secure Two-Party Computation
Authors:
Jesper Buus Nielsen,
Peter Sebastian Nordholt,
Claudio Orlandi,
Sai Sheshank Burra
Abstract:
We propose a new approach to practical two-party computation secure against an active adversary. All prior practical protocols were based on Yao's garbled circuits. We use an OT-based approach and get efficiency via OT extension in the random oracle model. To get a practical protocol we introduce a number of novel techniques for relating the outputs and inputs of OTs in a larger construction.
We…
▽ More
We propose a new approach to practical two-party computation secure against an active adversary. All prior practical protocols were based on Yao's garbled circuits. We use an OT-based approach and get efficiency via OT extension in the random oracle model. To get a practical protocol we introduce a number of novel techniques for relating the outputs and inputs of OTs in a larger construction.
We also report on an implementation of this approach, that shows that our protocol is more efficient than any previous one: For big enough circuits, we can evaluate more than 20000 Boolean gates per second. As an example, evaluating one oblivious AES encryption (~34000 gates) takes 64 seconds, but when repeating the task 27 times it only takes less than 3 seconds per instance.
△ Less
Submitted 14 February, 2012;
originally announced February 2012.
-
Superposition Attacks on Cryptographic Protocols
Authors:
Ivan Damgaard,
Jakob Funder,
Jesper Buus Nielsen,
Louis Salvail
Abstract:
Attacks on classical cryptographic protocols are usually modeled by allowing an adversary to ask queries from an oracle. Security is then defined by requiring that as long as the queries satisfy some constraint, there is some problem the adversary cannot solve, such as compute a certain piece of information. In this paper, we introduce a fundamentally new model of quantum attacks on classical cryp…
▽ More
Attacks on classical cryptographic protocols are usually modeled by allowing an adversary to ask queries from an oracle. Security is then defined by requiring that as long as the queries satisfy some constraint, there is some problem the adversary cannot solve, such as compute a certain piece of information. In this paper, we introduce a fundamentally new model of quantum attacks on classical cryptographic protocols, where the adversary is allowed to ask several classical queries in quantum superposition. This is a strictly stronger attack than the standard one, and we consider the security of several primitives in this model. We show that a secret-sharing scheme that is secure with threshold $t$ in the standard model is secure against superposition attacks if and only if the threshold is lowered to $t/2$. We use this result to give zero-knowledge proofs for all of NP in the common reference string model. While our protocol is classical, it is sound against a cheating unbounded quantum prover and computational zero-knowledge even if the verifier is allowed a superposition attack. Finally, we consider multiparty computation and show that for the most general type of attack, simulation based security is not possible. However, putting a natural constraint on the adversary, we show a non-trivial example of a protocol that can indeed be simulated.
△ Less
Submitted 31 August, 2011;
originally announced August 2011.
-
Fully Simulatable Quantum-Secure Coin-Flip** and Applications
Authors:
Carolin Lunemann,
Jesper Buus Nielsen
Abstract:
We propose a coin-flip protocol which yields a string of strong, random coins and is fully simulatable against poly-sized quantum adversaries on both sides. It can be implemented with quantum-computational security without any set-up assumptions, since our construction only assumes mixed commitment schemes which we show how to construct in the given setting. We then show that the interactive gener…
▽ More
We propose a coin-flip protocol which yields a string of strong, random coins and is fully simulatable against poly-sized quantum adversaries on both sides. It can be implemented with quantum-computational security without any set-up assumptions, since our construction only assumes mixed commitment schemes which we show how to construct in the given setting. We then show that the interactive generation of random coins at the beginning or during outer protocols allows for quantum-secure realizations of classical schemes, again without any set-up assumptions. As example applications we discuss quantum zero-knowledge proofs of knowledge and quantum-secure two-party function evaluation. Both applications assume only fully simulatable coin-flip** and mixed commitments. Since our framework allows to construct fully simulatable coin-flip** from mixed commitments, this in particular shows that mixed commitments are complete for quantum-secure two-party function evaluation. This seems to be the first completeness result for quantum-secure two-party function evaluation from a generic assumption.
△ Less
Submitted 23 June, 2011; v1 submitted 4 February, 2011;
originally announced February 2011.
-
Secure two-party quantum evaluation of unitaries against specious adversaries
Authors:
Frédéric Dupuis,
Jesper Buus Nielsen,
Louis Salvail
Abstract:
We describe how any two-party quantum computation, specified by a unitary which simultaneously acts on the registers of both parties, can be privately implemented against a quantum version of classical semi-honest adversaries that we call specious. Our construction requires two ideal functionalities to garantee privacy: a private SWAP between registers held by the two parties and a classical priva…
▽ More
We describe how any two-party quantum computation, specified by a unitary which simultaneously acts on the registers of both parties, can be privately implemented against a quantum version of classical semi-honest adversaries that we call specious. Our construction requires two ideal functionalities to garantee privacy: a private SWAP between registers held by the two parties and a classical private AND-box equivalent to oblivious transfer. If the unitary to be evaluated is in the Clifford group then only one call to SWAP is required for privacy. On the other hand, any unitary not in the Clifford requires one call to an AND-box per R-gate in the circuit. Since SWAP is itself in the Clifford group, this functionality is universal for the private evaluation of any unitary in that group. SWAP can be built from a classical bit commitment scheme or an AND-box but an AND-box cannot be constructed from SWAP. It follows that unitaries in the Clifford group are to some extent the easy ones. We also show that SWAP cannot be implemented privately in the bare model.
△ Less
Submitted 10 September, 2010;
originally announced September 2010.
