Keywords: formal methods, concurrent systems, Hoare logic
Unit: 24 credits
Background
Predicate transformer semantics were introduced by Dijkstra [Dij75]. They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Predicate transformer semantics are a reformulation of Floyd-Hoare logic [Flo67,Hoa69]. Whereas Floyd-Hoare logic is presented as a deductive system, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions) are complete strategies to build valid deductions of Floyd-Hoare logic. In other words, they provide an effective algorithm to reduce the problem of verifying a Hoare triple to the problem of proving a first-order formula.
Predicate transformers have been carried over to cope with concurrent systems [Lam90]
Research Questions and Tasks
Usually predicate transformers are used to prove (partial and total) correctness of programs, i.e. a program yields the desired final result. In a concurrent setting, this assumes that every components ‘plays according to the rules’.
The project aims at looking at the possibility of using the same techniques (predicate transformers) to reveal possible attack strategies. That means, given a ‘undesired state’ - a state an attacker would like to reach - can we calculate a strategy/program for an attacker to achieve this state. Ideally, a theoretical approach should be underlined by concrete examples.
References
- [Dij76] E.W. Dijkstra: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453-457, 1975. doi: 10.1145/360933.360975.
- [Hoa69] C.A.R. Hoare: Hoare, An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580, 1969. doi: 10.1145/363235.363259.
- [Flo67] R.W. Floyd. Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19, 19–31. 1967.
- [Lam90] L. Lamport: win and sin: Predicate Transformers for Concurrency. ACM Transactions on Programming Languages and Systems 12(3), 396-428, 1990.
Requirements: knowledge in the area of formal verification, e.g. Hoare logic