Abstract
Robotics is very appealing and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as maths, physics or electronics. Although this symbiotic relationship between robotics and programming is perceived as largely beneficial, educational approaches often feel the need to hide the underlying complexity of the robotic system, but as a result fail to transmit the reactive essence of robot programming to the roboticists and programmers of the future. This paper presents Rosy, a novel language for teaching novice programmers through robotics. Its functional style is both familiar with a high-school algebra background and a materialization of the inherent reactive nature of robotic programming. Working at a higher-level of abstraction also teaches valuable design principles of decomposition of robotics software into collections of interacting controllers. Despite its simplicity, Rosy is completely valid Haskell code compatible with the ROS~ecosystem. We make a convincing case for our language by demonstrating how non-trivial applications can be expressed with ease and clarity, exposing its sound functional programming foundations, and developing a web-enabled robot programming environment.

Abstract
Electronic Control Units are embedded devices that control various critical features of an automobile. Consequently, it is crucial to develop tools that enable penetration testers to identify security vulnerabilities within these ECUs as efficiently as possible. Fuzzing, a widely-used technique, can help uncover vulnerabilities in various types of applications. Fuzzing can then be applied to test ECUs through their communication protocols, the most common being the Controller Area Network (CAN). We present oCANada, a generation-based fuzzer which can be utilized in order to craft CAN messages for fuzzing. Many existing CAN fuzzers rely on simple mutation-based fuzzing, which involves randomly changing bits in the CAN payload. This paper introduces a novel generation-based fuzzing approach that leverages CAN database files (DBCs) in order to craft syntactically correct messages. oCANada also incorporates State-of-the-Art CAN reverse engineering techniques in order to enable syntax-aware fuzzing even when DBCs are not available. Additionally, this paper discusses test oracle techniques employed for fuzzing ECUs over CAN in both greybox and blackbox environments. Finally, we present our results while running the tool which we used two CANoe simulations, a Gateway ECU, and a modified version of the instrument cluster simulator ICSim. In these results, we also compare our fuzzer to the well-known CaringCaribou fuzzer.

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
We present a formally verified proof of the correctness and IND-CCA security of ML-KEM, the Kyber-based Key Encapsulation Mechanism (KEM) undergoing standardization by NIST. The proof is machine-checked in EasyCrypt and it includes: 1) A formalization of the correctness (decryption failure probability) and IND-CPA security of the Kyber base public-key encryption scheme, following Bos et al. at Euro S&P 2018; 2) A formalization of the relevant variant of the Fujisaki-Okamoto transform in the Random Oracle Model (ROM), which follows closely (but not exactly) Hofheinz, Hovelmanns and Kiltz at TCC 2017; 3) A proof that the IND-CCA security of the ML-KEM specification and its correctness as a KEM follows from the previous results; 4) Two formally verified implementations of ML-KEM written in Jasmin that are provably constant-time, functionally equivalent to the ML-KEM specification and, for this reason, inherit the provable security guarantees established in the previous points. The top-level theorems give self-contained concrete bounds for the correctness and security of ML-KEM down to (a variant of) Module-LWE. We discuss how they are built modularly by leveraging various EasyCrypt features.

Abstract
Conflict-free Replicated Data Types (CRDTs) are a very popular class of distributed data structures that strike a compromise between strong and eventual consistency. Ensuring the protection of data stored within a CRDT, however, cannot be done trivially using standard encryption techniques, as secure CRDT protocols would require replica-side computation. This paper proposes an approach to lift general-purpose implementations of CRDTs to secure variants using secure multiparty computation (MPC). Each replica within the system is realized by a group of MPC parties that compute its functionality. Our results include: i) an extension of current formal models used for reasoning over the security of CRDT solutions to the MPC setting; ii) a MPC language and type system to enable the construction of secure versions of CRDTs and; iii) a proof of security that relates the security of CRDT constructions designed under said semantics to the underlying MPC library. We provide an open-source system implementation with an extensive evaluation, which compares different designs with their baseline throughput and latency.

Abstract
Existing bidirectional languages are either state-based or operation-based, depending on whether they represent updates as mere states or as sequences of edit operations. In-between both worlds are delta-based frameworks, where updates are represented using alignment relationships between states. In this paper, we formalize delta lenses over inductive types using dependent type theory and develop a point-free delta lens language with an explicit separation of shape and data. In contrast with the already known issue of data alignment, we identify the new problem of shape alignment and solve it by lifting standard recursion patterns such as folds and unfolds to delta lenses that use alignment to infer meaningful shape updates. © Bidirectional Transformations 2012.