4th Workshop on
Hot Issues in Security Principles and Trust
Affiliated with ETAPS 2016
Eindhoven, The Netherlands
April 3rd, 2016
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.
Somesh Jha, University of
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.
|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|
|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|
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).
For information about registration, accommodation and travel please refer to the ETAPS web site.
Véronique Cortier (program chair): email.