Details: Speakers, titles and abstracts

Morning session: Blockchain

ALGORAND: The Blockchain for the Borderless Economy

By: Silvio Micali of MIT

Abstract:

Blockchains stand to revolutionize the way democratic societies and traditional economies operate. As currently implemented, however, blockchains are aspirational and cannot achieve their enormous potential.
Algorand is an alternative, democratic, and efficient blockchain. Its consensus protocol dispenses with ‘proof of work’ and ‘miners’; requires only a negligible amount of computation; guarantees that its transaction history does not ‘fork’ (i.e., guarantees the finality of all transactions); and allows for consensual evolution, so as to enable the community to meet its future needs without any ‘hard forks.’
Algorand is the first blockchain that is simultaneously secure, scalable and truly decentralized, and its deep roadmap will greatly augment the value of its platform.

Company Bio:

Based in Boston and founded by cryptography pioneer and Turing award winner Silvio Micali, Algorand is an open-source software company building technical innovation for the borderless economy with a platform that delivers decentralization, scalability and security. Algorand’s first-of-its-kind, permissionless, pure proof-of-stake protocol supports the scale, open participation, and transaction finality needed by users to build opportunity and fulfill the promise of blockchain technology.

Session: Blockchain Infrastructure

Tezos: self-amendment, formal verification and research time scales

by Michel Mauny, Board member, Tezos

Abstract:

Tezos' upgradability, through its self-amendment capabilities, and its strong links with formal verification allow it to interact with research on different time scales. In this presentation, I will recall the main features of the Tezos blockchain, and discuss its links with the world of research.
Affiliation: Nomadic Lacs <nomadic-labs.com>

Bio:

Michel is Chief Scientific Officer at Nomadic Labs, on leave from Inria (the French National Institute for Computer Science and Applied Mathematics), where he was a senior researcher and more recently Chief Executive Officer of the Inria Foundation. Michel is also a member of the Board of the Tezos Foundation. Michel’s scientific interests are mainly in the fields of programming languages: design, implementation, semantics, static analysis, and type systems. After his Ph.D. at Paris-Diderot University, Michel joined Inria in 1985 and worked on programming languages with the research group that designed and developed OCaml, the functional programming language used to implement Tezos, and the Coq proof assistant. From 1989 to 2005, Michel led the research team that further developed OCaml, and he has been a Professor of Computer Science at Ensta-ParisTech from 2005 to 2016.

Plutus — Functional Smart Contracts on Cardano

by Manuel Chakravarty, Blockchain Language Architect, IOHK

Abstract

Functional programming and blockchains are a match made in heaven! The immutable and reproducible nature of distributed ledgers is mirrored in the semantic foundation of functional programming. Nevertheless, most existing blockchains favour an object-oriented, imperative approach to contract specification and execution, although it is widely understood that this style of programming comes with a range of safety and security pitfalls in the context of concurrent and distributed systems.

In this talk, I will outline how IOHK’s Plutus team combines programming language theory, functional programming, and domain-specific languages to develop a radically new approach to blockchain contract development. This not only helps us to reason about safety and security, it also provides an integrated and flexible approach to smart contracts and decentralised applications that offers something to a broad range of users, from software developers to domain experts.

Bio

Manuel M T Chakravarty has published extensively on programming languages, compilers, and high-performance computing. He contributed to both the design and implementation of the Haskell programming language as well as several Haskell tools and open source libraries. With the increasing adoption of functional programming in industry, he shifted his focus to unlocking new application areas for functional programming and helping development teams reap the benefits of modern programming language technology. He is currently co-leading the research-driven Plutus smart contract language team at IOHK.

IOHK

Founded in 2015 by Charles Hoskinson and Jeremy Wood, IOHK is a technology company committed to using peer-to-peer innovations to provide financial services to the three billion people who don’t have them. We are an engineering company that builds cryptocurrencies and blockchains for academic institutions, government entities and cooperations. We are a decentralised company that loves small, innovative teams forming and executing ideas that cause cascading disruption.

Session: Blockchain Ecosystem

Turning A Vehicle Into An Economic Platform

by Michael Huth, CTO, XAIN

Abstract:

Consumer expectations and fierce market competition have led to margins becoming increasingly thinner for manufacturers of consumer and commercial vehicles. These actors realize now more than ever, that the value of their goods no longer rests on the basic functions they provide, but rather on the types and qualities of user experiences they can offer: extra horse-power on demand, ability to share usage, selling data streams to third parties - to name a few.

Increasingly, manufacturers are exploring ways to capture this value by turning a vehicle into a mini-economic platform that facilitates value exchange. Usage of that platform must be controlled so that value creation and consumption are neither impeded, nor corrupted, for the tenants that interact on it.

Our R&D in policy-based access control, distributed ledger technology, and embedded systems has led to the development of FROST Technology for fully programmable sharing ecosystems and flexible usage control on a vehicle’s compute systems. FROST can thus provide consumers with novel, on-demand services whilst enabling manufacturers to tap into additional revenue streams.

Bio:

Michael Huth is CTO of XAIN AG and a Professor of Computer Science in the Department of Computing at Imperial College London. He is a Diplom-Mathematiker (TU Darmstadt, Germany), obtained his PhD in 1991 (Tulane University of Louisiana, USA), completed several postdoctoral studies internationally, and was an Assistant Professor at Kansas State University. His present research focuses on cybersecurity, especially on the interplay of trust, security, risk, and economics. He was the Technical Lead of the Theme Harnessing Economic Value in the UK PETRAS IoT Cybersecurity Research Hub. Professor Huth is also active as a research and product advisor in the London Cybersecurity startup scene.

About XAIN:

XAIN AG was incorporated in February 2017 in Germany. It is a Berlin-based startup that does research in cybersecurity and machine learning. XAIN prevailed over 120+ competitors to win the 1st Porsche Innovation Contest in 2017. XAIN successfully completed a pilot with Porsche in March 2018 that brought blockchain technology into a Porsche Panamera. XAIN's Strategic Partnership with Infineon was announced in October 2018 to bring such innovation into microcontroller technology as used in vehicles. XAIN has a 20+ workforce of which 60% are engineers.

Session: Verified Smart Contracts

Formal Design, Implementation and Verification of Blockchain Languages

by Grigore Risu, CEO, Runtime Verification

Abstract:

Many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses of the underlying blockchain programming languages or virtual machines. The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal specification. We demonstrate the feasibility of the proposed approach by applying it to two blockchains, Ethereum and Cardano.

Bio:

Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the president and CEO of Runtime Verification, Inc (RV). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000. He was offered the CAREER award by the NSF, the Dean's award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper), the Runtime Verification test of time award (for an RV 2001 paper), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002.

Modularity for Accurate Static Analysis of Smart Contracts

by Mooly Sagiv: Certora and Tel Aviv University

Abstract

Static code analysis is a useful technique for finding bugs in code and proving their absence. Existing industrial tools sacrifice precision which leads to false errors reported and missed bugs.

I will describe a new way to perform accurate static analysis (ASA) of smart contracts in order to identify bugs and prove their absence before the code is deployed. ASA guarantees that all bugs are reported and that all errors are real. ASA operates on bytecode programs which enables to check the code even when the source is not available.

Scalability of the method is guaranteed by verifying each of the contracts with respect to the requirements of other contracts.

Bio:

Mooly Sagiv is a CEO of Certora Ltd. and a chair of software systems at Tel-Aviv University. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. He received numerous scientific awards for contributions static program analysis including Bessel award, ACM fellow, Microsoft Research Outstanding Collaborator Award, and senior ERC grant.

Verified Oak smart contracts

by Bas Spitters

Abstract:

Concordium's Oak/Acorn smart contract language is a member of the ML-family of programming languages. This language is functional and has no run-time exceptions, thus avoiding a large class of bugs. We have embedded this language in the Coq proof assistant. This allows us to give mathematical proofs about Oak smart contracts. For instance, we have shown that an Oak implementation of the infamous TheDAO contract is not vulnerable to a large class of attacks.

Bio:

Bas Spitters is associate professor computer science at Aarhus University, WP leader in the Concordium Blockchain Research Center and
Concordium's Chief Scientific Advisor formal verification and smart contracts. He holds a PhD in mathematics from Nijmegen University (2003), has received an elite Veni grant by Dutch NWO. He has served as work package leader of the ForMath EU project to make the formalization of
mathematics feasible at scale, and has written over 40 refereed publications.

Project:

The Concordium blockchain network (https://www.concordium.com/) is the first business-friendly ID/KYC-enabled blockchain ledger. Features include: private proof of stake and the functional Oak smart contract language which has no run time exceptions. The Concordium Foundation funds the Blockchain Research Centre at Aarhus University (https://concordium.au.dk). The driving goal of the research center is to provide the basic research needed to build energy-efficient and scalable blockchain technology that is provably secure. http://www.cs.au.dk/~spitters/