High(er) assurance blockchains: functional and performance verification in the software design process

Conference:	Verification Futures 2018 (click here to see full programme)
Speaker:	Dr Neil Davies, Chief Scientist, Predictable Network Solutions Ltd
Presentation Title:	High(er) Assurance Blockchains: Functional and Performance Verification in the Software Design Process
Abstract:	The Cardano project is delivering a distributed-ledger proof-of-stake blockchain system as high-assurance software. Central to this assurance is a chain of formal and semi-formal evidence, linking the peer-reviewed blockchain protocol Ouroboros-Praos to deployable Haskell code via a series of refinement steps. The blockchain protocol relies on distribution of data between nodes of the system with real-time performance criteria that we capture using the ∆Q framework. The design process that we are attempting relies on being able to formally describe versions of the protocol in such a way that we can simulate or execute them, reason formally about relationships between different versions, and do abstract performance evaluations in the ∆Q framework. This enables step by step design refinement, with rapid prototyping, whilst ensuring at each step that we can meet our functional and performance criteria. This talk will give an overview of this process, the lessons learned and the progress so far towards this ambitious goal. Blockchains are trusted repositories for data having significant value Their security, liveness and utility is tied to their performance Building formal verification directly into the design and development cycle reduces total lifecycle costs
Speaker Bio:	Neil Davies is an expert in resolving the practical and theoretical challenges of large scale distributed and high-performance computing, particularly scalability effects in large distributed systems, their operational quality, and how to manage their degradation gracefully under saturation and adverse operational conditions. He is a computer scientist, mathematician and hands-on software developer who builds rigorously engineered working systems and scalable demonstrators of new computing and networking concepts. Throughout his 20-year career at the University of Bristol he was involved with early developments in networking, its protocols and their implementations. He collaborated with organisations such as NATS, Nuclear Electric, HSE, ST Microelectronics and CERN on issues relating to scalable performance and operational safety. He was also technical lead on several large EU Framework collaborations relating to high performance switching. He has mentored PhD candidates at CERN, and is currently assisting with Ph.D. candidates at the University of Catalonia. He co-founded Degree2 Innovations in 2000, commercialising network QoS research, and went on to found Predictable Network Solutions in 2003. He has worked on performance aspects of the Department of Defense’s Future Combat Systems project, and has developed approaches to delivering consistent video telephony for sign language users over retail broadband. He is the co-author of several patent families.