posted by organizer: nowakd || 4702 views || tracked by 6 users: [display]

ENTROPY 2019 : ENabling TRust through Os Proofs… and beYond

FacebookTwitterLinkedInGoogle

Link: https://entropy2019.sciencesconf.org
 
When Jun 16, 2019 - Jun 16, 2019
Where Stockholm, Sweden
Submission Deadline Mar 15, 2019
Notification Due Apr 10, 2019
Final Version Due Apr 22, 2019
Categories    operating systems   theorem provers   security   verification
 

Call For Papers

**************************************************************************
Final Call for papers — ENTROPY 2019
ENabling TRust through Os Proofs … and beYond

Second International workshop on the use of theorem provers for modelling
and verification at the hardware-software interface

https://entropy2019.sciencesconf.org

Co-located with EuroS&P'19, KTH, Stockholm, June 2019
**************************************************************************

INVITED SPEAKERS

Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge

IMPORTANT DATES

Paper submission: March 15, 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019

AIM AND SCOPE

Low level software such as kernels and drivers, along with the hardware
this software runs on, is critical for application security. In contrast
with user applications, OS kernel software runs in privileged CPU mode
and is thus highly critical. Large projects such as seL4, VeriSoft,
CertiKoS and Prosper have invested considerable resources in developing
formally verified systems such as hypervisors and microkernels, supplying
proofs that they satisfy critical properties. Such proofs are delicate in
terms of the scale and complexity of real systems, the models used in
performing the proof search, and the relations between the two, which
recent vulnerabilities such as Spectre and Meltdown have shown to be a
highly non-trivial issue.

The purpose of this workshop is to share, compare and disseminate best
practices, tools and methodologies to verify OS kernels, also setting the
stage for future steps in the direction of fully verified systems,
dealing with issues related to modelling, model validation, and large
proof maintenance through system evolution. On one hand, we need to make
low-level proofs more scalable, modular and cost-effective. On the other
hand, once certified systems are available, preservation and maintenance
of their proofs of validity become key questions.

The goal of the ENTROPY workshop is to provide a forum for researchers
and practitioners in this space, linking operating systems, formal
methods, and hardware architecture, interested in system design as well
as machine verified mathematical proofs using proof assistants such as
Coq, Isabelle and HOL4.

This will be the second edition of the ENTROPY workshop series. The
first workshop was organised by the Pip Development Team at University
of Lille in 2018.

TOPICS OF INTEREST

Specific topics include, but are not limited to:

* Verified kernels and hypervisors
* Verified security architectures and models
* Tools and frameworks for hardware security analysis
* Tools and frameworks for security analysis
* Formal hardware models and model validation techniques
* Theorem prover based tools and frameworks for verification of low level code
* Combinations of static analysis and theorem proving
* Theories and techniques for compositional security analysis
* Case studies and industrial experience reports
* Proof maintenance techniques and problems
* Compositional models and verification techniques
* Proof oriented design

The aim of the workshop is to stimulate innovation and active exchange
of ideas, so position papers, work-in-progress and industrial
experience submissions are welcome.

SUBMISSION AND PUBLICATION

There are two categories of submissions:

1. Regular papers describing fully developed work and complete results
(10 pages, references included, IEEE format)

2. Short papers, position papers, industry experience reports,
work-in-progress submissions (4 pages, references included, IEEE
format)

All papers should be in English and describe original work that has not
been published or submitted elsewhere. The submission category should
be clearly indicated. All submissions will be fully reviewed by members
of the Programme Committee. Papers will appear in IEEE Xplore in a
companion volume to the regular EuroS&P proceedings. For formatting and
submission instructions see https://entropy2019.sciencesconf.org.

PROGRAM CHAIRS

Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille

PROGRAM COMMITTEE

Christoph Baumann, Ericsson AB
Gustavo Betarte, Univ. de la República, Uruguay
David Cock, ETH Zurich
Mads Dam, KTH Royal Institute of Technology (chair)
Anthony Fox, ARM
Deepak Garg, MPI Saarbrucken
Ronghui Gu, Columbia University
Samuel Hym, Univ. Lille
Thomas Jensen, INRIA and Univ. Rennes
Toby Murray, Univ. Melbourne
David Nowak, CNRS & Univ. Lille (chair)
Vicente Sanchez-Leighton, Orange Labs
Thomas Sewell, Chalmers

Related Resources

Security 2025   Special Issue on Recent Advances in Security, Privacy, and Trust
IEEE COINS 2024   IEEE COINS 2024 - London, UK - July 29-31 - Hybrid (In-Person & Virtual)
IJIS Special Issue 2024   Reinforcing Cyber Security of Critical Infrastructures through Digital Twins
CSW 2024   2024 3rd International Conference on Cyber Security
ICHST--Ei 2024   2024 6th International Conference on Hardware Security and Trust (ICHST 2024)
CEVVE 2024   2024 2nd International Conference on Electric Vehicle and Vehicle Engineering (CEVVE 2024)
IEEE ICC'24 NextG-WiSec 2024   IEEE NextG-WiSec: The Ninth IEEE Workshop on NextG (6G and beyond) Wireless Security in conjunction with IEEE ICC 2024, 9–13 June 2024 - Denver, CO, USA
ECTIJ 2024   Economics, Commerce and Trade Management: An International Journal
Relations 2024   Relations. Beyond Anthropocentrism
WiMob - CWN 2024   Eleventh International Workshop on Cooperative Wireless Networks (WiMob – CWN’24)