Software Verification

For digital trust to work in practice, the underlying design and implementation need to work even in adversarial scenarios. Formal verification tools systematically analyse all possible scenarios in a formally defined threat model. They can automatically identify previously overlooked lines of attack that require changes to protocols and designs. In the final system, they can mathematically prove that the system continues to deliver the desired functionality in all scenarios. A particular strength of formal verification tools is that they ensure, in combination with compilers and a runtime platform, that the desired functionality is correctly implemented in code running on the deployed system. This approach prevents some of the most widespread cyber-attacks that result from software vulnerabilities such as buffer overflows and ensures that correct high-level protocols cannot be subverted due to implementation bugs.

In this pillar we aim to work on practical formal verification tools applicable to software in general, as well as verified platform that will help industry make a leap towards bullet-proof software implementing digital trust services. Our methodology stems from an observation that the only practical approach to verified software is embedding verification in the software development process itself, by deploying verifiers that work along the compilers and development environments and increasing the automation of verification to make it non-intrusive for developers. We aim to deliver verification tools that can prove safety, security, and privacy properties in an increasingly broad set of scenarios. We also aim to develop techniques to verify specific properties and libraries of interest for the financial industry, for data mining in pharmaceutical industry, and for automated processing of large value chains.

To take one possible example, consider how the emergence of smart contracts (on platforms such as Ethereum) amplifies the need to obtain high confidence in program correctness. When “code is the law”, a mistake in the code can lead to the collapse of an autonomous entity. Indeed, the spectacular logical error in the smart contract program defining the Distributed Autonomous Organization, DAO, has led not only to loss of investment but to forking of the underlying blockchain, shaking the trust in the Ethereum market.

Several prominent players in smart contracts have well recognized the need for verification and validation tools and are engaging with academic collaborators to drive their development. These tools can be used to validate smart contracts, transaction protocols, as well as software implementations of clients performing blockchain computations. Several industrial users have recognized the Scala programming language, developed at EPFL, as a great platform for smart contracts, which makes verification tools such as of immediate interest for creating trustworthy smart contracts. At the same time, we aim to improve our verification techniques and apply them to a diverse set of software layers and applications, because benefits of verified software are the greatest when applied to the entire software stack.

DuoKey, Futurae and Nym join the C4DT through its associate partner program

We are delighted to announce that 3 additional start-ups have joined the C4DT community through the C4DT start-up program. For two years Duokey SA, Futurae Technologies AG and Nym Technologies SA will complement the already diverse group of partner companies through their start-up perspectives to collaborate and share insights on…
News type : News

Ruag AG joins the C4DT

We are pleased to announce that Ruag AG, Switzerland, has just joined the C4DT as partner. Owned by the Confederation, Ruag AG is the technology partner of the Swiss Armed Forces. Together with armasuisse, Ruag’s presence strengthens C4DT's expertise in cybersecurity and cyber defense. We are convinced that this partnership…
News type : News

Trust Valley sets off at EPFL

An alliance for excellence supported by multiple public, private and academic actors, the "TRUST VALLEY" was launched on Thursday, October 8, 2020. Cantons, Confederation, academic institutions and captains of industry such as ELCA, Kudelski and SICPA, come together to co-construct this pool of expertise and encourage the emergence of innovative…
News type : News

Vaud and Geneva join forces to create the Trust Valley

Building on the expertise of 300 companies and 500 experts, the Vaud and Geneva Cantons of Switzerland are launching the Trust Valley, a public private cooperation for safe digital transformation, cybersecurity and innovation. Among the founding partners are C4DT members ELCA, Kudelski Group and SICPA. For more information please click…
News type : News

CYD and EPFL launch the CYD Fellowships

Cyber-threats have been accelerating due to the exponential growth of network connectivity. These new capabilities provide myriad opportunities for security hackers to wreak significant damage for commercial, political, or other gains. To promote research and education in cyber-defence, EPFL, the Swiss Federal Institute of Technology in Lausanne, and the Cyber-Defence…
News type : News

C4DT mentioned in “Le Temps” as an initiative against cybercrime

Initiatives against cybercrime, online harassment or spying are increasing at an impressive rate. Switzerland wants to position itself as a world center of excellence. French-language news paper 'Le Temps' asked Olivier Crochat, executive director of the Center for Digital Trust, about the center's focus. Read the article in French on…
News type : Press reviews

C4DT mentioned in RTS French radio show Alter Eco

C4DT is mentioned in RTS French radio show 'Alter Eco', broadcasted on Jan 6th in French and entitled "Lausanne, 'capital mondial de la confiance'". Please click below to access the broadcast.
News type : Press reviews

Switzerland: launch of a label to protect SMEs from cyber risks

Protecting your SME from cyberattacks is often complicated: costs of IT security audits, absent or overly complex standards, lack of internal skills have discouraged more than one company from confronting these risks. Born from a participative approach, the Label helps SMEs and other small organizations to manage their cyber…
News type : News

Launch of the CyberPeace Institute in Geneva

Thursday 26 September 2019 saw the launch of the CyberPeace Institute, an independent NGO that will address the growing impact of major cyberattacks, assist vulnerable communities, promote transparency, and advance global discussions on acceptable behavior in cyberspace. EPFL President Martin Vetterli will be sitting on the Executive Board, and the…
News type : News

C4DT’s academic director on e-ID in “Le Temps” daily newspaper

On the 4th of June, the Council of States debated the Swiss law on e-ID (Federal Act on Electronic Identification Services, LSIE). C4DT’s academic director Prof. Jean-Pierre Hubaux wrote an article on the topic for the Swiss French-language daily newspaper 'Le Temps', in which he favors state control of all…
News type : Press reviews

EPFL computer scientists flag global hardware security vulnerability

Researchers in the HexHive and Parallel Systems Architecture (PARSA) laboratories of EPFL's School of Computer and Communication Sciences, in collaboration with IBM researchers, have identified a widespread computer security vulnerability affecting laptop, desktop and server hardware.
News type : News

The daily newspaper “Le Temps” interviews the Center for Digital Trust

"Many SMEs are discovering digitalization but are not armed to deal with the threats that accompany this process." The Swiss French-language daily newspaper “Le Temps” interviewed C4DT's executive director, Dr. Olivier Crochat, and academic director, Prof. Jean-Pierre Hubaux, on the mission and ambitions of this new center, based at EPFL,…
News type : Press reviews

C4DT Holds First General Assembly

The founding General Assembly of C4DT was held on Friday, 2 November, in presence of the President of EPFL, Martin Vetterli, and of 50 guests. The 12 partners of the Center said they are keen to apply research to their business needs and regulatory requirements, at a time when digitalization…
News type : News