Opendata, web and dolomites

CIRCUS SIGNED

An end-to-end verification architecture for building Certified Implementations of Robust, Cryptographically Secure web applications

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

Project "CIRCUS" data sheet

The following table provides information about the project.

Coordinator
INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE 

Organization address
address: DOMAINE DE VOLUCEAU ROCQUENCOURT
city: LE CHESNAY CEDEX
postcode: 78153
website: www.inria.fr

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country France [FR]
 Total cost 1˙885˙248 €
 EC max contribution 1˙885˙248 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2015-CoG
 Funding Scheme ERC-COG
 Starting year 2016
 Duration (year-month-day) from 2016-04-01   to  2021-03-31

 Partnership

Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE FR (LE CHESNAY CEDEX) coordinator 1˙885˙248.00

Map

 Project objective

The security of modern web applications depends on a variety of critical components including cryptographic libraries, Transport Layer Security (TLS), browser security mechanisms, and single sign-on protocols. Although these components are widely used, their security guarantees remain poorly understood, leading to subtle bugs and frequent attacks. Rather than fixing one attack at a time, we advocate the use of formal security verification to identify and eliminate entire classes of vulnerabilities in one go. With the aid of my ERC starting grant, I have built a team that has already achieved landmark results in this direction. We built the first TLS implementation with a cryptographic proof of security. We discovered high-profile vulnerabilities such as the recent Triple Handshake and FREAK attacks, both of which triggered critical security updates to all major web browsers and TLS libraries. So far, our security theorems only apply to carefully-written standalone reference implementations. CIRCUS proposes to take on the next great challenge: verifying the end-to-end security of web applications running in mainstream software. The key idea is to identify the core security components of web browsers and servers and replace them by rigorously verified components that offer the same functionality but with robust security guarantees. Our goal is ambitious and there are many challenges to overcome, but we believe this is an opportune time for this proposal. In response to the Snowden reports, many cryptographic libraries and protocols are currently being audited and redesigned. Standards bodies and software developers are inviting researchers to help analyse their designs and code. Responding to their call requires a team of researchers who are willing to deal with the messy details of nascent standards and legacy code, and at the same time prove strong security theorems based on precise cryptographic assumptions. We are able, we are willing, and the time is now.

 Publications

year authors and title journal last update
List of publications.
2017 Jonathan Protzenko, Cédric Fournet, Nikhil Swamy, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan
Verified low-level programming embedded in F*
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3110261
Proceedings of the ACM on Programming Languages 1/ICFP 2019-06-18
2017 Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
A messy state of the union
published pages: 99-107, ISSN: 0001-0782, DOI: 10.1145/3023357
Communications of the ACM 60/2 2019-06-18
2016 Karthikeyan Bhargavan, Cedric Fournet, Markulf Kohlweiss
miTLS: Verifying Protocol Implementations against Real-World Attacks
published pages: 18-25, ISSN: 1540-7993, DOI: 10.1109/MSP.2016.123
IEEE Security & Privacy 14/6 2019-06-18
2017 Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi
Formal Modeling and Verification for Domain Validation and ACME
published pages: 561-578, ISSN: , DOI: 10.1007/978-3-319-70972-7_32
Financial Cryptography and Data Security 2019-04-18

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "CIRCUS" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "CIRCUS" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.1.)

PROGRESS (2019)

The Enemy of the Good: Towards a Theory of Moral Progress

Read More  

SuperH (2019)

Discovery and Characterization of Hydrogen-Based High-Temperature Superconductors

Read More  

InsideChromatin (2019)

Towards Realistic Modelling of Nucleosome Organization Inside Functional Chromatin Domains

Read More