Correlated randomness is a ubiquitous resource in cryptography. A one-time pad, namely a pair of identical random keys, enables perfectly secure communication. More complex forms of correlated randomness can similarly facilitate protocols for secure multiparty computation that allow two or more parties to jointly compute a function of secret inputs …
read moreOther presentations
Security evaluation of industrial control systems using system emulation and fuzzing
Recent years have been pivotal in the field of Industrial Control Systems (ICS) security, with a large number of high-profile attacks exposing the lack of a design-for-security initiative in ICS, as well as a substantial number of research works that try to proactively uncover underlying vulnerabilities. The main focus on …
read moreA Semantic Model for Interacting Cyber-Physical Systems
We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes. Our semantic model uniformly exposes externally observable behaviors of components expressed as sets of sequences of observations. We introduce algebraic operations on such sequences …
read moreSymbolic Execution Formally Explained
The topic of this talk is a formal explanation of symbolic execution in terms of a symbolic transition system and prove its correctness and completeness with respect to an operational semantics which models the execution on concrete values. I will first introduce a formal model for a basic programming language …
read moreVerification of Distributed Epistemic Gossip Protocols (2)
Gossip protocols are concerned with the spread of knowledge in a social network. They aim at arriving, by means of point-to-point or group communications, at a situation in which all agents know each other's secrets.
We consider distributed gossip protocols that are expressed in a simple programming language that employs …
read moreOn Dynamic Software Updates
Software updates are dynamic if they are applied at run time. In this talk, we present ongoing work on dynamic updates for modular software. In the last decades, most research on dynamic software updates propose a practical update framework for specific monolithic software (such as C or Java programs). In …
read moreReasoning about call-by-value recursive procedures in Hoare logic
Basic Hoare logic, without recursive procedures, admits proofs of correctness that are linear in the size of the program under consideration. This is why proof outlines, which annotate programs with assertions that must hold of intermediate states, are so useful. In this talk, we discuss how to reason about programs …
read morePwoP: Intrusion-Tolerant and Privacy-Preserving Sensor Fusion
We design and implement, PwoP, an efficient and scalable system for intrusion-tolerant and privacy-preserving multi-sensor fusion. PwoP develops and unifies techniques from dependable distributed systems and modern cryptography, and in contrast to prior works, can 1) provably defend against pollution attacks where some malicious sensors lie about their values to …
read moreIntegrating ADTs in KeY and their Application to History-based Reasoning
We discuss integrating abstract data types (ADTs) in the KeY theorem prover, and how to reason about the correctness of the Java Collection interface using histories. We introduce a new method to model histories logically (using the Isabelle theorem prover), and translate inferred rules to user-defined taclets in KeY to …
read more