Abstract

Abstract
This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

Abstract
We propose a hybrid formal verification approach that combines high-level deductive reasoning and circuit-based reasoning and apply it to highly optimized cryptographic assembly code. Our approach permits scaling up formal verification in two complementary directions: 1) it reduces the proof effort required for low-level functions where the computation logics are obfuscated by the intricate use of architecture-specific instructions and 2) it permits amortizing the effort of proving one implementation by using equivalence checking to propagate the guarantees to other implementations of the same computation using different optimizations or targeting different architectures. We demonstrate our approach via an extension to the EasyCrypt proof assistant and by revisiting formally verified implementations of ML-KEM in Jasmin. As a result, we obtain the first formally verified implementation of ML-KEM that offers performance comparable to the fastest non-verified implementation in x86-64 architectures.

Abstract

Abstract
This workshop proposal is the third edition of a workshop which has been organised at EICS 2023 and EICS 2024. This edition aims to bring together researchers and practitioners interested in the engineering of interactive systems that embed AI technologies (as for instance, AI-based recommender systems) or that use AI during the engineering lifecycle. The overall objective is to identify (from experience reported by participants) methods, techniques, and tools to support the use and inclusion of AI technologies throughout the engineering lifecycle for interactive systems. A specific focus is on guaranteeing that user-relevant properties such as usability and user experience are accounted for. Contributions are also expected to address system-related properties, including resilience, dependability, reliability, or performance. Another focus is on the identification and definition of software architectures supporting this integration.

Abstract