formal methods
Fulvio Valenza (Politecnico di Torino)
Formal and Automatic Network Security Configuration
The next-generation networks introduced higher flexibility and dynamicity in networking systems, but at the same time, they led to new threats and challenges. The traditional approach of a manual configuration of Network Security Functions (NSFs) such as firewalls and VPN gateways is not feasible anymore since it is not adequate for the ever-changing nature of modern networks and it is prone to human errors. To overcome this problem, the native flexibility provided by virtualization could be exploited to automate network security management. However, achieving a high level of automation while providing formal assurance that security management operations (e.g., configuration and orchestration) fulfill some security properties is still a complex research challenge. This presentation describes some novel approaches that combine automation, formal verification, and optimization for network security management. This is a joint seminar with FM-SEC. Attendance via Zoom (ID: 933 8257 2879, Passcode: 546836) Livestream via Youtube
Muhammad Usama Sardar (TU Dresden)
Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing
ZoomConfidential Computing (CC) using hardware-based Trusted Execution Environments (TEEs) has emerged as a promising solution for protecting sensitive data in all forms. One of the fundamental characteristics of such TEEs is remote attestation which provides mechanisms for securely measuring and reporting the state of the remote platform and computing environment to a user. We present a novel approach combining TEE-agnostic attestation architecture and formal analysis enabling comprehensive and rigorous security analysis of attestation mechanisms in CC. We demonstrate the application of our approach for three prominent industrial representatives, namely Arm Confidential Compute Architecture (CCA) in architecture lead solutions, Intel Trust Domain Extensions (TDX) in vendor solutions, and Secure CONtainer Environment (SCONE) in frameworks. For each of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism in confidential computing, namely provisioning, initialization, and attestation protocol. Our approach reveals design and security issues in Intel TDX and…
Massimo Merro (UniVR)
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…