62 documents found, page 1 of 7

Application of recurrent neural networks in uncertainty analysis of sheet metal...

The quality of deep-drawn sheet metal components can be strongly influenced by different sources of uncertainty, such as variations in process conditions, deviations in tool geometry, and variations in material properties between coils. Identifying the underlying causes of forming defects remains a challenging and time-consuming task due to the complexity of the forming process. This study presents a machine le...

Formally verifying Kyber. Episode IV: implementation correctness

In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present hi...

A formal treatment of the role of verified compilers in secure computation

Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a...

Use of Antithrombotics at the End of Life

N/a.; N/a.

Machine-checked ZKP for NP relations: formally verified security proofs and imp...

MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protoco...

Coming out em pessoas lgb com 55+ anos : uma revisão sistemática de literatura

Certified compilation for cryptography: Extended x86 instructions and constant-...

We present a new tool for the generation and verification of high-assurance high-speed machine-level cryptography implementations: a certified C compiler supporting instruction extensions to the x86. We demonstrate the practical applicability of our tool by incorporating it into supercop: a toolkit for measuring the performance of cryptographic software, which includes over 2000 different implementations. We sh...

The last mile: High-Assurance and High-Speed cryptographic implementations

We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as handwritten assembly. We illustrate our approach using ChaCha20Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outpe...

Decentralized privacy-preserving proximity tracing

[Excerpt] This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale. This system provides a technological foundation to help slow the spread of SARS-CoV-2 by simplifying and accelerating the process of notifying people who might have been exposed to the virus so that they can take appropriate measures to break its transmission chain. The system aims to mini...

Em torno de uma engenharia cidadã

Apesar da estranheza do tema e do modo como é formulado, o meu propósito resume-se a poucas palavras: pensar uma engenharia com dimensão cidadã, feita para os cidadãos e com os cidadãos, no âmbito das preocupações com a construção de futuros sustentáveis e com a ética da conservação/preservação dos patrimónios que recebemos em herança.