Seminar - Value-dependent information-flow security on weak memory models
School of Engineering and Computer Science Seminar
Speaker: Dr. Graeme Smith
Time: Tuesday 16th April 2019 at 11:00 AM - 12:00 PM
Location: Cotton Club, Cotton 350
Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not it is secure. This is particularly the case in programs where the security levels of variables are value-dependent, i.e., depend on the values of other variables. This talk will illustrate how instruction reordering allowed by contemporary multicore processors leads to vulnerabilities in such programs, and will present a compositional information flow logic which can be used to detect such vulnerabilities. The logic allows step-local reasoning (one instruction at a time) about a thread's security by incorporating a dependency relation between variables indicating when an assignment to one variable is guaranteed to have occurred earlier than that to another. Program security can then be established from individual thread security using rely/guarantee reasoning.
- Graeme Smith is an Associate Professor at the University of Queensland, Australia. His research interests lie in the area of formal methods. Since 2013 he has focused on the application of formal methods to concurrent programs, and in particular concurrent programs running on hardware weak memory models. This work has included methods for verifying the functional correctness of programs, and more recently their security.