- More Information for better utility; less information for better privacy; ARC Discovery with CC Morgan, Vanessa Teague and Steve Schneider (2014—16)
- Making software more reliable using a new model for entropies of computers’ internal state; ARC Discovery with CC Morgan and Joost-Pieter Katoen (2012—14)
PhD and MRes Projects
There are a number of PhD and MRes projects available. See below for details:
SCIENCE: Computing – More information for better utility; less information for better privacy. Details here.
Controlling and Designing Software Defined Networks (Master of Research/PhD in Computer Science/Engineering)
Software Defined Networks (SDNs) allow network administrators to have programmable central control of network traffic via a controller without requiring physical access to the network’s switches. A configuration of an SDN can create a logical network control where hardware is physically decoupled from the data forwarded, i.e. network switches follow the rules given by the controller and only forward packets by the given rules.
Research Question and Tasks
Up to date network configuration often requires the manual configuration of each and every router, which entails a high maintenance cost. For SDNs, however, there are prototypic languages which can manage parts of the configuration of routers automatically (e.g. NetCore http://frenetic-lang.org). Although language support exists, it is still unknown how effective and how usable these languages are.
Aim of the project is to analyse the capabilities of such a language and use the language to formalise contem- porary network routing.
The ideal applicant should be interested in applying Formal Methods and logic-based calculi in general. Prior knowledge about SDNs is not needed.
The project will be a cooperation between Macquarie University and NICTA. Close collaboration with industry partners ensures the use-inspired nature of the project.
Software Verification Tool Suite for Protocol Development (Master of Research/PhD in Computer Science/Engineering)
Software verification is a discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements. Since software becomes more complex, verification tasks become even more important. Software verification often starts with verifying specifications from which implementations are derived later on.
However, this requires that specifications is free of ambiguities and contradictions. Using English prose only, this is nearly impossible to achieve and hence every specification should be equipped with a formal specification.
We have developed AWN, a language particularly tailored for the specification of routing protocols. After an unambiguous specification is given, it can be analysed and verified by verification tools, such as model checking or interactive theorem provers. Input for these tools have so far be derived manually.
It is our belief that AWN should be used right from the beginning when designing protocols. Even more it should be possible to do a quick analysis of the protocol already during the first phase of development. But, this can only be achieved if tools support the development.
Research Question and Tasks
The aim of the project is to develop a software verification tool suite for protocol development. This framework should include an easy-to-use interface for writing specifications as well as an automatic analysis running in the background. For the project we will use external tools such as the model checker Uppaal and the interactive theorem prover Isabelle. Hence it is part of the project to combine the tool suite with these tools. Optionally, the project can also include the development of simple test cases that can be used to perform a first analysis of the developed protocol.
The ideal applicant should have experience in programming and good knowledge about software architecture. Prior knowledge about formal methods (model checking and theorem proving) and networks/protocols is not required and will be explained when needed; however basic understanding of mathematical formulas is needed.
The project will be a cooperation between Macquarie University and NICTA.