[TYPES/announce] CFP VerifyThis Long-Term Challenge (VTLTC 2020)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Presentations VerifyThis Long-Term Challenge 2020 - Concluding Event - co-located with ETAPS and VerifyThis 25th and 26th April 2020, Dublin, Ireland http://verifythis.github.io/ Deadline: 1st March 2020 ## Introduction The VerifyThis Long-Term Challenge complements the on-site format of the VerifyThis competition with a verification challenge, in which teams contribute to the verification of a practically relevant piece of software over a period of six months. The challenge aims to be a showcase that deductive program verification can produce relevant results for real systems with acceptable effort. The challenge 2020 started in September 2019, and ends February 2020. To conclude the challenge, we will have a final workshop session at ETAPS along with the VerifyThis program verification competition [1]. For 2020, the challenge system is the new, implementation of the PGP server infrastructure, called HAGRID [2]. The old implementation did not conform to GDPR and was known to be vulnerable against DoS attacks. We invite you to present your results on the verification of this security-relevant challenge system during a special session of the VerifyThis program verification competition, held at ETAPS. ## Submission Authors are invited to submit a presentation proposal (or extended abstract) as a PDF using Springer’s LNCS style, which should be about a page long, but not longer than three pages (excluding bibliography). It should discuss ... * ... the used verification approach and tools * ... how the challenge was adapted to make verification possible (abstractions, reimplementation, different behaviour) * ... what has been achieved (modelled and verified properties) * ... successes and challenges encountered in the course of the case study. ## Submission Link https://easychair.org/conferences/?conf=vtltc2020 ## Proceedings There will be an informal pre-proceeding of the accepted presentation proposals. A special issue for this verification challenge is planned and will be discussed on-site. ## Important dates Submission deadline: 1st March 2020 Notifications: 15th March 2020 Workshop: 25-26th April 2020 ## Program Chairs and Organizers Marieke Huisman Raul E. Monti Mattias Ulbrich Alexander Weigl [1] https://www.pm.inf.ethz.ch/research/verifythis.html [2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/
[TYPES/announce] HotSpot: Hot Topics in the Principles of Security and Trust
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [ type-oriented theories have played a big role in the principles of security and trust in the past, and we welcome work in this area to HotSpot! --Joshua ] HotSpot, which we intend as a blend of invited and contributed papers, has now confirmed a list of excellent invited speakers, grouped into three areas: Privacy and quantitative information flow Giovanni Cherubin (EPFL) Pasquale Malacaria (QMUL) Secure Compilation Catalin Hritcu (INRIA) Frank Piessens (KU Leuven) Voting protocols and privacy-type properties Steve Kremer (INRIA) Carsten Schürmann (ITU Copenhagen) We're looking for a similar number of contributed talks to fill out the day. They may be on related topics, or range across other aspects of the principles of security and trust. This is shaping up to be a very promising exchange of ideas on security and trust principles. We'd love to have your submission for a talk about the work you're most interested in right now. Talks may cover work published elsewhere, or work to be published elsewhere. Alternately, if you'd like your paper to be published as a HotSpot paper, we can offer slots in the IEEE Xplore digital library area for the IEEE Euro S workshops. The deadline for submission is: 28 February All the details are below. See also http://hotspot.compute.dtu.dk Looking forward to the event; please join in! Joshua and Sebastian = HotSpot 2020: 6th Workshop on Hot topics in the Principles of Security and Trust Affiliated with Euro S 2020, 15th of June 2020 in Genova, Italy http://hotspot.compute.dtu.dk Organized by the Theory of Security working group IFIP WG 1.7. = Aim and scope = The principles of security and trust remain an area of intense and creative work. This work is focused primarily on defining security and trust goals, developing methods to verify the systems meet those goals, and to synthesize systems that meet those goals by construction. The areas of interest for HotSpot cut across many application areas, including hardware-software connections, distributed and cloud systems, big data, machine learning for (and against) security and privacy, and single-purpose systems such as voting, electronic currency and smart contracts. The areas of interest are unified however by a focus on rigorous models and reasoning, clear semantics, and a balance between proof and empirical methods. Format == The one-day workshop will be divided into a sequence of four main sessions. Each session will be devoted to a set of talks on related topics, both with invited talks and submitted papers. The sessions are 1. Privacy and quantitative information flow (C Palamidessi) 2. Voting protocols and privacy-type properties (P Y A Ryan, S Mödersheim) 3. Secure compilation (P Degano) 4. Open session Submissions on all formally-grounded topics related to security, privacy and trust are welcome. They can either be (a) an informal submission, consisting of an abstract or a paper that may appear formally elsewhere. (b) a full submission, to be included in an IEEE Xplore volume accompanying the main IEEE EuroS 2020 proceedings. See submission instructions on our website: http://hotspot.compute.dtu.dk PC == Catherine Meadows Catuscia Palamidessi Jan Juerjens Joshua Guttman (co-chair) Matteo Maffei Peter Y A Ryan Pierpaolo Degano Sebastian Mödersheim (co-chair) Jean-Jacques Quisquater Steve Schneider Veronique Cortier Important Dates === Workshop papers submission: February 28, 2020 Workshop notification date: April 12, 2020 Workshop date: June 15, 2020 Submission instructions === See http://hotspot.compute.dtu.dk -- Who sups with the devil should bring a long spoon.
[TYPES/announce] Call For Participation to TYPES-ITRS 2020: early registration expires on 16th February
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == 26th INTERNATIONAL CONFERENCE ON TYPES FOR PROOFS AND PROGRAMS 2020 - 2-5 MARCH 10th WORKSHOP ON INTERSECTION TYPES AND RELATED SYSTEMS - 6 MARCH == https://types2020.di.unito.it Turin, Italy The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * foundations of type theory and constructive mathematics; * applications of type theory; * dependently typed programming; * industrial uses of type theory technology; * meta-theoretic studies of type systems; * proof assistants and proof technology; * automation in computer-assisted reasoning; * links between type theory and functional programming; * formalizing mathematics using type theory. We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. The EUTypes Cost Action CA15123 (eutypes.cs.ru.nl) focuses on the same research topics as TYPES and partially sponsors the TYPES Conference: Part of the program is organised under the auspices of EUTypes. INVITED SPEAKERS * Ulrik Buchholtz * Pierre Marie-Pédrot * Leonardo de Moura * Sara Negri The ITRS 2020 workshop aims to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches. Possible topics for submitted papers include, but are not limited to: * Formal properties of systems with intersection types. * Results for related systems, such as union types, refinement types, or singleton types. * Applications to lambda calculus, pi-calculus and similar systems. * Applications for programming languages, program analysis, and program verification. * Applications for other areas, such as database query languages and program extraction from proofs. * Related approaches using behavioural/intensional types and/or denotational semantics to characterize computational properties. * Quantitative refinements of intersection types. Invited Speaker - Jeremy Siek Registration form: https://types2020.di.unito.it/registration.html *Early registration: 16th February* CONTACT Email: ugo.deligu...@unito.it -- Ugo de'Liguoro Associate Professor Dept. of Computer Science University of Torino Corso Svizzera 185, 10149, Torino (Italy) phone +39 011 6706766 - fax +39 011 751603
[TYPES/announce] Postdoc position: verified timing-channel security for seL4
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Postdoc position: verified timing-channel security for seL4 http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security Applications close: February 25, 09:00 AM Australian Eastern Daylight Time (AEDT; GMT +11) Timing channels plague modern systems, undermining their security. Yet no operating system provides provable protection against them. We believe that seL4 can be the first kernel to meet this challenge [1], building on its world-first proof of confidentiality enforcement [2] and its unique mechanisms for implementing time protection [3]. The seL4 project is seeking a highly motivated postdoctoral researcher to investigate methods for proving that operating system kernels can defend against timing channels. We are seeking somebody with a research background in formal methods and security. You will contribute to the development of methods for reasoning about timing channels in verified operating system kernels, applied to the seL4 kernel. Your work will also investigate how to extend seL4’s existing proofs of information flow security, which primarily cover storage channels, to also encompass timing channels. Further details about the research project are summarised in the following position paper: [1] Gernot Heiser, Gerwin Klein and Toby Murray. "Can We Prove Time Protection?" in Proceedings of the Workshop on Hot Topics in Operating Systems (HotOS), pages 23-29, May 2019. https://arxiv.org/abs/1901.08338 The position is for two years in the first instance, based at the University of Melbourne under Dr Toby Murray (https://people.eng.unimelb.edu.au/tobym/). You will work with a close-knit team here at University of Melbourne, and collaborate heavily with UNSW and Data61’s Trustworthy Systems group, in Sydney. Candidates should have experience in at least one of the following: - program verification (e.g. Hoare logic) - information flow security (e.g. non-interference) - interactive theorem provers (e.g. Isabelle, Coq, etc.) Applications close on February 25, 09:00 AM Australian Eastern Daylight Time (AEDT; GMT +11) To apply, or fore more information, visit: http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security Informal enquiries should be directed to Toby Murray toby.mur...@unimelb.edu.au https://people.eng.unimelb.edu.au/tobym/ References [1] Gernot Heiser, Gerwin Klein and Toby Murray. "Can We Prove Time Protection?", HotOS 2019 [2] Toby Murray, et al. "seL4: From General Purpose to a Proof of Information Flow Enforcement", IEEE Symposium on Security and Privacy 2013 [3] Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser. "Time Protection: The Missing OS Abstraction", EuroSys 2019
