Update, August 2016: the workshop report is now available.
Many security problems can be solved reliably only using formal methods. This workshop considers the relationship between the rapidly improving techniques of formal methods and the problems of information (in)security. It will bring together people with expertise ranging from core information security problems to the techniques of formal methods, with many flavors of overlap in between.
The workshop will be primarily a forum for discussion and interaction. It will be loosely divided into four problem areas: Hardware Architecture, Distributed Systems, Privacy, and Operating Systems. The workshop is by invitation only.
The workshop participants will assess the currently most pressing problems in a range of security areas, and the formal methods that can make a difference to them. In particular, workshop discussion may include:
- Major security problems that may be amenable to formal methods, their logical character, and the promising formal methods for problems of this type.
- Assessing the scale of real-world problems, and the problem sizes that might be amenable by formal methods now or in a few years.
- Identifying major problems that are not amenable to current techniques, and exploring ideas or abstractions that might guide contemporary rigorous techniques to resolve them.
- Defining "success" for formal methods for these problems, including the security guarantees than might be obtained.
- Identification of new (and possibly clean slate) approaches to applying formal methods to security problems.
The workshop produced a report on the opportunities for substantial increase of the use of formal methods across security problems.