Invited Talks
Anna Slobodova
Microcode Verification - Another Piece of the Microprocessor Verification Puzzle
Despite significant progress in formal hardware verification in the past decade, little has been published on the verification of microcode. Microcode is the heart of every microprocessor and is one of the most complex parts of the design: it is tightly connected to the huge machine state, written in an assembly-like language that has no support for data or control structures, and has little documentation and changing semantics. At the same time it plays a crucial role in the way the processor works.
We describe the method of formal microcode verification we have developed for an x86-64 microprocessor designed at Centaur Technology. While the previous work on high and low level code verification is based on an unverified abstract machine model, our approach is tightly connected with our effort to verify the register-transfer level implementation of the hardware. The same microoperation specifications developed to verify implementation of the execution units are used to define operational semantics for the microcode verification. While the techniques that we use are not inherently new, to our knowledge, our effort is the first interconnection of hardware and microcode verification in context of an industrial size design. Both our hardware and microcode verifications are done within the same framework.
Short Bio
Anna Slobodova leads the formal verification group at Centaur Technology (www.centtech.com), which is, based in Austin, Texas. Centaur designs x86-compatible VIA Nano microprocessor. In the last six years, the formal verification team has built a variety of custom tools on top of ACL2 system to enhance validation of the Nano design at the micro-architectural, transistor and microcode levels. Before joining Centaur Technology, Dr. Slobodova spent seven years at Intel, where she was involved with the formal verification of several Intel processor designs. In the 1990s, she was one of the industrial, formal-methods pioneers as a part of the Alpha development team at DEC and at Compaq. In the previous years she was an assistant professor at the University of Trier, Germany.
Anna Slobodova holds PhD in Computer Science from Comenius University, Bratislava, Slovakia. She has served as a program committee member for a number various conferences concerned with formal methods, e.g., Computer-Aided Verification (CAV) and Formal Methods in Computer-Aided Design (FMCAD). Dr. Slobodova served as a FMCAD co-chair in 2011.
Rod Chapman
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK.
This paper presents a retrospective of our experiences with applying theorem proving to the verification of SPARK programs, both in terms of projects and the technical evolution of the language and tools over the years.
Short Bio
Roderick Chapman is a Principal Engineer with Altran UK, specializing in the design and implementation of safety and security-critical systems. He currently leads the programming language design and static analysis tools group at Altran.
Peter Sewell
Retrofitting Rigour
We rely on an enormous number of software components, which continue to be developed ---as they have been since the 1940s--- by methods based on a test-and-debug cycle and informal-prose specifications. Replacing this legacy infrastructure and development practices wholesale is not (and may never be) feasible, so if we want to improve system quality by using mathematically rigorous methods, we need a strategy to do so incrementally. A first step is to focus on the more stable extant interfaces: processor architectures, programming languages, and key APIs, file formats, and protocols. By characterising these with new precise abstractions, we can start to retrofit rigour into the system, using those (1) to improve existing components by testing, (2) as interfaces for replacement formally verified components, and (3) simply to gain understanding of what the existing behavioural interfaces are. Many issues arise in building such abstractions and in establishing confidence in them. To validate them against existing systems, they must be made executable, not necessarily in the conventional sense but as test oracles, to check whether observed behaviour of the actual system is admitted by the specification. The appropriate treatment of loose specification is key here, and varies from case to case. To validate them against the intent of the designers, they must be made broadly comprehensible, by careful structuring, annotation, and presentation. And to support formal reasoning by as broad a community as possible, they must be portable into a variety of reasoning tools. Moreover, the scale of real-world specifications adds further engineering concerns. This talk will discuss the issues of loose specification and some lessons learnt from developing and using our Ott and Lem lightweight specification tools, which are aimed at supporting all these pre-proving activities (and which target multiple theorem provers).
Short Bio
Peter Sewell is a Professor of Computer Science and an EPSRC Leadership Fellow at the University of Cambridge Computer Laboratory. He held a Royal Society University Research Fellowship from 1999-2007, and took his PhD in Edinburgh in 1995, supervised by Robin Milner.