4th Workshop on
Hot Issues in Security Principles and Trust
(HotSpot 2016)
ETAPS 2016

Affiliated with ETAPS 2016
Eindhoven, The Netherlands
April 3rd, 2016

Scope - Important dates - Invited talks - Accepted papers - Program - Proceedings - PC - Submissions - Registration, accommodation and travel - Previous Editions of HotSpot - Contact


This workshop is intended to be a less formal counterpart to the Principles of Security and Trust (POST) conference at ETAPS, and with an emphasis on "hot topics", both of security and of its theoretical foundations and analysis.

Like POST, the themes are:

Submissions about new and emerging topics (for example, those that have not appeared prominently in conferences and workshops until now) are particularly encouraged. Submissions of preliminary, tentative work are also encouraged. There is no page limit, but the length of your submission should be appropriate to its content. There will be no formal proceedings. Inclusion in informal proceedings is optional.

This workshop is organized by IFIP WG 1.7: Theoretical Foundations of Security Analysis and Design.

Important dates

Invited talk

Somesh Jha, University of Wisconsin and IMDEA Software and Bill Harris, Georgia Institute of Technology:
Synthesis techniques for security
The problem of implementing a secure program is an ideal problem domain for formal methods. Even a small error in the logic of a program can drastically weaken the security guarantees that it provides. Existing work on applying formal methods to security has focused primarily on applying verification techniques to determine if an existing program satisfies a desired security guarantee. In this talk, we propose that many problems in secure programming can instead be addressed by synthesizing a provably-secure program automatically.
We review our work on automatically instrumenting programs that satisfy security properties expressible as safety properties and on a general framework for designing program synthesizers. We then describe a potential line of work on automatically synthesizing programs that satisfy two-trace hyperproperties, a key class of properties that formulate information-flow policies with declassification but are not supported by current program synthesizers.


SUNDAY April 3rd
09:15 - 9:30 Welcome
Invited talk Chair: Véronique Cortier
09:30 - 10:30 Synthesis techniques for security
Somesh Jha (University of Wisconsin and IMDEA Software)
10:30 - 11:00 Coffee break
Session I Chair: Pierpaolo Degano
11:00 - 11:30 Localizing Security for Distributed Firewalls
Pedro Adão, Riccardo Focardi, Joshua Guttman and Flaminia Luccio
11:30 - 12:00 Principles of Layered Attestation
Paul Rowe
12:00 - 12:30 Securing IoT communications: at what cost?
Chiara Bodei and Letterio Galletta
12:30 - 14:00 Lunch
Session II Chair: Riccardo Focardi
14:00 - 14:30 Learning and Verifying Unwanted Behaviours
Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton and Igor Muttik
14:30 - 15:00 Towards Safe Enclaves
Neline van Ginkel, Raoul Strackx, Jan Tobias Muehlberg and Frank Piessens
15:00 - 15:30 Coffee break
Session III Chair: Peter Ryan
15:30 - 16:00 Measuring Protocol Strength with Security Goals
Paul Rowe, Joshua Guttman and Moses Liskov
16:00 - 16:30 A Method for Verifying Privacy-Type Properties: The Unbounded Case
Lucca Hirschi, David Baelde and Stéphanie Delaune
16:30 - 17:00 Verification of privacy-type properties for security protocols with XOR
David Baelde, Stéphanie Delaune, Ivan Gazeau and Steve Kremer
17:00 - 18:00 WG 1.7 business meeting
Workshop dinner


The proceedings are now available.


The only mechanism for paper submissions is via the electronic submission web-site powered by easychair.
Please, follow the instructions given there (note, in particular, that only pdf files may be submitted).

Program Committee

Registration, accommodation and travel

For information about registration, accommodation and travel please refer to the ETAPS web site.

Previous Editions of HotSpot


Véronique Cortier (program chair): email.