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

Scope

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:

• theory of computer security;
• formal specification, analysis and design of security systems;
• automated reasoning for security analysis.

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

• Submission: January 8, 2016 January 16, 2016 (extended)
• Author Notification: February 19, 2016
• Final versions for informal proceedings (optional): March 4th, 2016
• Workshop: April 3rd, 2016

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.

Program

Program

The proceedings are now available.

Submissions

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

• Hubert Comon-Lundh, ENS Cachan, France
• Véronique Cortier, CNRS, Loria, France
• Cas Cremers, University of Oxford, UK
• Pierpaolo Degano, University of Pisa, Italy
• Riccardo Focardi, Ca' Foscari University, Italy
• Sibylle Froeschle, OFFIS & University of Oldenburg, Germany
• Joshua Guttman, Worcester Polytechnic Institute, USA
• Boris Köpf, IMDEA Software Institute, Spain
• Ralf Küsters, University of Trier, Germany
• Cathy Meadows, Naval Research Laboratory, USA
• Charles Morisset, Newcastle University, UK
• Peter Y. A. Ryan, University of Luxembourg
• Pierangela Samarati, University of Milano, Italy
• Steve Schneider, University of Surrey, UK
• Geoffrey Smith, Florida International University, USA

Registration, accommodation and travel

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

Previous Editions of HotSpot

• HotSpot 2015
• HotSpot 2014
• HotSpot 2013

Contact

Véronique Cortier (program chair): email.