Security and Safety in Distributed Systems

Security and Safety in Distributed Systems

The concurrency, the communication and the information flow in distributed systems are a source of design errors that affect the systems' trustworthiness. We focus on formal analyses for qualitative and quantitative aspects of security and safety:

Formal Analysis of Security in Distributed Systems
Security specifications of systems introduce the requirements for their availability, confidentiality and integrity properties. These properties are attained by appropriate mechanisms, including cryptographic protocols and countermeasures against known threats such as the Denial of Service (DoS) attack. We formally analyze the security of cryptographic protocols and attack countermeasures by model checking a system model including the behavior of an intruder. The tools used in this research are the Spin model checker and the PRISM probabilistic model checker. As an intruder, we consider a malicious entity that attempts to alter the system's services or possibly halt it, or even to access confidential information.

An intruder model with the hardest possible assumptions for the dominance over the communication between the security protocol participants

In [BKP07], [BKP10] and [BKP11] we introduced intruder models for verifying secrecy and authentication properties of cryptographic protocols based on the hardest possible assumptions for the dominance of the intruder over the communication between the protocol participants. We proposed heuristics in order to overcome the state space explosion, due to the high non-determinism of the intruder's behavior.

In [BKP08] and [BKP09] we introduced an attacker model for quantitative verification of DoS attacks against cryptographic protocols using probabilistic model checking. We evaluate the level of resource expenditure for the attacker, beyond which the likelihood of widespread attack is reduced and compare design considerations for optimal resistance to the DoS threat.

In [ADB10] and [DKB11] we analyzed attacks against the Domain Name System (DNS) using probabilistic model checking. [ADB10] refers to the analysis of the highly publicized Kaminsky DNS Cache Poisoning Attack, whereas [DKB11] refers to the analysis of a distributed DoS attack known as DNS Bandwidth Amplification, and its countermeasures. Attack countermeasures are compared by applying an extensive Cost-Benefit Analysis.

In [BPA11] we introduced a Continuous-Time Markov Chain for studying the Certified E-mail Message Delivery protocol in constrained environments. Using probabilistic model checking, it is possible to adjust security configurations in order to provide sufficient protection and to simultaneously satisfy service performance requirements.

In the SPHINX project, model checking was used  to detect security policy flaws, due to interactions between the measures for countering SPam over Internet Telephony and the SIP protocol ([SBK11], [GKB12]). In [SSK13] we focused on the audio CAPTCHAs vulnerability to DoS attacks, due to their excessive bandwidth demands. DoS can be mitigated by appropriate admission control policies that were compared through a Cost-Benefit Analysis based on probabilistic model checking results.

Contact person: Prof. Panagiotis Katsaros
Joint work with: Prof. Scott Smolka, Prof. Dimitris Gritzalis, Prof. Giorgos Papadimitriou, Prof. Andreas Pombortsis, Dr. Stylianos Basagiannis, Dr. Sophia Petridou, Dr. Tushar Deshpande, Dr. Yannis Soupionis, Dr. Anakreon Mentis, Emmanouela Stachtiari, Nikos Alexiou    

Verification and code generation for transaction processing with the
ACID Model Checker & Code Generator ([MK09], [MK12])

Formal Analysis of Safety in Distributed Systems
When the services delivered in a distributed system fail, this may have catastrophic consequences on the system's users. To cope with the problems associated with concurrency and communication, the programmers rely on protocols and algorithms that provide high-level guarantees for the computations, such as atomicity, consistency, isolation and fault tolerance. These guarantees are often relaxed in computing environments with resource constraints and long communication delays. Moreover, various domain-specific guarantees have to be provided, like the fairness in electronic payments. We have proposed techniques for the formal analysis of systems and the generation of correct-by-construction code for interlocking control, transaction processing and electronic payment services. The tools used in this research are the Spin model checker and the CPN Tools for editing, simulating and analyzing Colored Petri Nets.

In [MK09] and [MK12] we introduced the ACID Model Checker & Code Generator, a tool for the specification and validation of transaction models that supports the generation of provably correct code for transaction processing. In [KOG05] and [KAT09] we proposed an approach for building and validating Colored Petri Net models of electronic payments by model checking payment transaction guarantees like money conservation, distributed payment atomicity, certified delivery, fairness etc.

In [BKP06] we proposed an interlocking control protocol based on what we called Distributed Signal Boxes. The safety of the new protocol was validated using the Spin model checker. 

Contact person: Prof. Panagiotis Katsaros
Joint work with: Prof. Maria Gousidou-Koutita, Dr. Stylianos Basagiannis, Dr. Anakreon Mentis, Vasilis Odontidis

Information Flow and Inference Control in Distributed Systems
The . . .

Home | Projects | Publications | Partners | Related Links | News | People | Contact copyright � 2012 DSG group