Availability by Design: A Complementary Approach to Denial-of-Service

Roberto Vigo

Research output: Book/ReportPh.D. thesisResearch

471 Downloads (Pure)

Abstract

In computer security, a Denial-of-Service (DoS) attack aims at making a resource unavailable. DoS attacks to systems of public concern occur increasingly and have become infamous on the Internet, where they have targeted major corporations and institutions, thus reaching the general public. There exist various practical techniques to face DoS attacks and mitigate their effects, yet we witness the successfulness of many.
The need for a renewed investigation of availability gains in relevance when considering that our life is more and more dominated by Cyber-Physical Systems (CPSs), large-scale network of sensors that interact with the physical environment. CPSs are increasingly exploited in the realisation of critical infrastructure, from the power grid to healthcare, traffic control, and defence applications. Such systems are particularly prone to DoS attacks: in addition to classic communication-based attacks, their components can be subject to physical capture. Moreover, sensors are often powered by batteries, and time-limited unavailability is usually a stage planned to prolong their life span.
This dissertation argues that techniques rooted in the theory and practice of programming languages, language-based techniques, offer a unifying framework to deal with the consequences of DoS, thereby encompassing inadvertent and malicious sources of unavailability in a uniform manner.
In support to this claim we develop a family of process calculi, the Quality Calculi, where availability considerations are promoted to be first-class object of the language domain. Moreover, these modelling tools are complemented by static analyses that pinpoint where and why unavailability may occur, levering the enhanced expressiveness of the language.
The ultimate aim of the framework is to foster the development of systems resilient to DoS by means of a principled design process, in which formal models allow, and verification tools enforce, the production of such robust code.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages190
Publication statusPublished - 2015
SeriesDTU Compute PHD-2014
Number353
ISSN0909-3192

Cite this