The Security project is investigating the use of domain-specific languages and formal verification to describe and understand the properties of programs that manipulate secure information. Our approaches are based on formal semantic definitions of the information that is revealed by program operations, originally developed by Carroll Morgan. We are applying these semantic frameworks to simple languages for expressing algorithms such as cryptographic protocols and secure information exchange.
Anthony Sloane (Macquarie)
Annabelle McIver (Macquarie)
Carroll Morgan (University of NSW)
Anstractions of non-interference security: Probabilistic versus Possibilistic. T. S. Hoang, A. K. McIver, L. Meinicke, C. C. Morgan, A. Sloane and E. Susatyo. Formal Aspects of Computing, in press.