Latest Past Seminars

Attacking the Buyers and the Sellers: A Tale of Offline Readers and Payees’ Authentication

First, we will  look at security  analyses we performed against the Square Terminal (https://squareup.com/gb/en/hardware/terminal ), a well-sold PoS (point of sale), when set in offline mode (i.e., not connected to the Internet/payments networks when transactions occur).  We show that we can make the PoS work contrary to its EU/UK specifications (with relatively little technical effort), and --in so doing-- we are able to bypass customer authentication (PIN, fingerprint, etc.), and make illicit transactions. In this case of *offline* PoS, the victims are merchants, as well as plastic-cards’ holders. The attacks affect both Visa and Mastercard. Via responsible disclosure, we liaised with all stakeholders, and SquareUp is receptive.  Then, we will also look, in more detail than before, at how EU vs UK specification work. All these aspects were also supported by formal verification , which we discuss as well. This is a joint seminar with FM-SEC. Attendance via Zoom (ID: 967 1945…

Read more

Certifying Statistical Robustness in Coq

Robustness properties are a class of statistical properties that specify that perturbations in the input data should not significantly affect the result of a statistical method.  In this presentation, we explore our work in verifying claims robust mean estimators in Coq, from the seminal work of Tukey in the 1960s showing robustness bounds for the trimmed mean algorithm, as well as ongoing work in verifying more recent claims of robustness.  In the process, we have contributed new probability lemmas of the coq-infotheo library for information theory, and -- in order to better handle the probability theory of more advanced algorithms -- we present a new library for probability theory based on Lebesgue Measure theory that is being integrated into MathComp-analysis. This is a joint seminar with FM-SEC. Attendance via Zoom (ID: 919 9142 2762, Passcode: 245778) Livestream via Youtube

Formal methodologies to secure cyber-physical systems: from static analysis to runtime enforcement

We present some research works over the past nine years on applying formal methods to secure cyber-physical systems (CPSs). The presentation will take place at a sufficiently high level of detail and will essentially be divided into three parts. In the first part, we highlight an hybrid process calculus to model both CPSs and physics-based attacks. We formalize a threat model that specifies MITM attacks that can manipulate sensor readings and/or control commands in order to drive a CPS into an undesired state, and we provide the means to assess attack tolerance/vulnerability with respect to a given attack.  We then formalize how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. In the second part, we report a line of work that uses model checking tools and statistical model checking techniques to perform static security analysis of CPSs…

Read more