Automated Analysis of Security in Networking Systems | Mikael Buchholtz
| | Abstract | It has for a long time been a challenge to built secure networking systems. One way to counter this problem is to provide developers of software applications for networking systems with easy-to-use tools that can check security properties before the applications ever reach the marked. These tools will both help raise the general level of awareness of the problems and prevent the most basic flaws from occurring. This thesis contributes to the development of such tools.
Networking systems typically try to attain secure communication by applying standard cryptographic techniques. In this thesis such networking systems are modelled in the process calculus LySa. On top of this programming language based formalism an analysis is developed, which relies on techniques from data and control ow analysis. These are techniques that can be fully automated, which make them an ideal basis for tools targeted at non-experts users. The feasibility of the techiques is illustrated by a proof-of-concept implementation of a control ow analysis developed for LySa. From a techincal point of view, this implementation also interesting because it encodes in nite sets of algebraic terms, which denote encryption, as a nite number of tree grammar rules.
The security of any software application relies crucially on the scenario in which the application is deployed. In contrast to many related analysis approaches, this thesis provides an explict mechanism for specifying deployment scenarios. Even though these scenarios may be arbitrarily large the analysis techniques can be extended to cope with such scenarios. The analysis techniques are furthermore capable of tackling security issues that arise because of attacks from arbitrary attackers: the analysis can deal with con dentiality and authentication properties, parallel session attacks, and attacks launched by insiders.
Finally, the perspectives for the application of the analysis techniques are discussed, thereby, coming a small step closer to providing developers with easy- to-use tools for validating the security of networking applications. | | Type | Ph.D. thesis [Academic thesis] | | Year | 2004 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-PHD-2004-141 | | Note | Supervised by Prof. Hanne Riis Nielson and Prof. Flemming Nielson | | Electronic version(s) | [pdf] [ps] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|