Abstract
EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post-quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

Abstract

Abstract
Conflict-free Replicated Data Types (CRDTs) are abstract data types that support developers when designing and reasoning about distributed systems with eventual consistency guarantees. In their core they solve the problem of how to deal with concurrent operations, in a way that is transparent for developers. However in the real world, distributed systems also suffer from other relevant problems, including security and privacy issues and especially when participants can be untrusted. In this paper we present new privacy-preserving CRDT protocols that can be used to help secure distributed cloud-backed applications, including NoSQL geo-replicated databases. Our proposals are based on standard CRDTs, such as sets and counters, augmented with cryptographic mechanisms that allow their operations to be performed on encrypted data. We accompany our proposals with formal security proofs and implement and integrate them in An-tidoteDB, a geo-replicated NoSQL database that leverages CRDTs for its operations. Experimental evaluations based on the Danish Shared Medication Record dataset (FMK) exhibit the tradeoffs that our different proposals make and show that they are ready to be used in practical applications.

Abstract

Abstract
This tool paper presents the High-Assurance ROS (HAROS) framework. HAROS is a framework for the analysis and quality improvement of robotics software developed using the popular Robot Operating System (ROS). It builds on a static analysis foundation to automatically extract models from the source code. Such models are later used to enable other sorts of analyses, such as Model Checking, Runtime Verification, and Property-based Testing. It has been applied to multiple real-world examples, helping developers find and correct various issues.

Abstract
The vast datasets produced in human genomics must be efficiently stored, transferred, and processed while prioritizing storage space and restore performance. Balancing these two properties becomes challenging when resorting to traditional data compression techniques. In fact, specialized algorithms for compressing sequencing data favor the former, while large genome repositories widely resort to generic compressors (e.g., GZIP) to benefit from the latter. Notably, human beings have approximately 99.9 percent of DNA sequence similarity, vouching for an excellent opportunity for deduplication and its assets: leveraging inter-file similarity and achieving higher read performance. However, identity-based deduplication fails to provide a satisfactory reduction in the storage requirements of genomes. In this article, we balance space savings and restore performance by proposing GenoDedup, the first method that integrates efficient similarity-based deduplication and specialized delta-encoding for genome sequencing data. Our solution currently achieves 67.8 percent of the reduction gains of SPRING (i.e., the best specialized tool in this metric) and restores data 1.62x faster than SeqDB (i.e., the fastest competitor). Additionally, GenoDedup restores data 9.96x faster than SPRING and compresses files 2.05x more than SeqDB.