ResearchResearch AreasFormal Methods for Trustworthy Systems

Formal Methods for Trustworthy Systems

Leader:  Prof. Ron van der Meyden

Other Staff Members: Prof Gernot Heiser, Prof Carroll Morgan, Dr Kai Engelhardt, Dr Kevin Elphinstone, Dr Gabi Keller, Dr Xiao.

Development of scientific foundations for security and trustworthiness, characterising in precise terms what it means for an ICT system to be secure and trustworthy in the context of an adversarial environment. Even in cryptography, the most mathematically precise area of computer security, many issues remain to be addressed in formal security models, long-term secure and post-quantum algorithms and protocols, machine-verifiable computationally sound reductionist proofs, usability and user-oriented models, side-channel models, and efficient implementation in software and hardware.

Complementary and collaborative work in this program is lead by Prof Gernot Heiser (seconded from CSE) at NICTA. NICTA focus in this area is on highly trustworthy software, starting with the strong foundation of the formally-verified OS kernel, and working towards being able to make system-wide safety/security guarantees. This research has potential to increase system robustness and reduce the cost of verified software to the point where in a number of domains it will be cheaper than traditionally-engineered low-assurance software. Other collaborative work with CSE include formal concurrency models for verifying real-world systems, and formal modelling and verification of network and crypto protocols.

CYBER SECURITY AND PRIVACY LABORATORY
SCHOOL OF COMPUTER SCIENCE AND ENGINEERING
UNSW SYDNEY NSW 2052 AUSTRALIA TELEPHONE +61 2 9385 4329