[NB. This talk is on Friday, instead of the usual Tuesday slot.]

The next talk in the Galois Tech Seminar series:

• Date: Friday, November 13th, 2009
• Title: Hoare-Logic – fiddly details and small print
• Speaker: Rod Chapman
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/11/04/chapman-hoare/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

Presented by Julien Schmaltz.

Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.

Correct-By-Construction Control Synthesis in Model-Based Design of Autonomous Systems

speaker: Ufuk Topcu

abstract: How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional "design+verify" approach to "specify+synthesize" in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid dynamics that are subject to rich temporal logic specifications and heterogenous uncertainties, and that operate in adversarial environments. They combine ideas from control theory with those from computer science, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. The expressivity of the resulting design methodology enables us to formally investigate a number of emerging issues in autonomous, networked systems. I conclude my talk with a brief overview of several such issues from my ongoing projects: (i) compositional synthesis for the so-called fractionated systems; (ii) effects of perception imperfections on protocol synthesis; (iii) interfaces between learning modules and reactive controllers with provable guarantees of correctness; and (iv) human-embedded autonomy.

bio: Ufuk Topcu is a Research Assistant Professor in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. from the University of California, Berkeley and was a Postdoctoral Scholar at the California Institute of Technology until 2012. His research is on the analysis, design, and verification of autonomous, networked systems.

Formal Verification of Cyber-Physical Systems

speaker: Pavithra Prabhakar

abstract: Cyber-Physical Systems (CPS) refer to systems in which control, computation and communication converge to achieve complex functionalities. The ubiquitous deployment of cyber-physical systems in safety critical applications including aeronautics, automotive, medical devices and industrial process control, has pressurized the need for the development of automated analysis methods to aid the design of high-confidence systems. The talk will focus on an important feature of cyber-physical systems, namely, the mixed discrete-continuous behaviors manifesting as a result of the interaction of a network of embedded processors with the physical world. Hybrid Automata are a popular formalism for modeling systems exhibiting both discrete and continuous behaviors. We discuss formal approaches for the verification of hybrid automata. More precisely, scalable approaches based on approximations, including predicate abstraction, counter-example guided abstraction refinement and bounded error approximations, will be discussed in the context of safety and stability analysis. We will present applications of the techniques on hybrid automata models.

bio: Pavithra Prabhakar is on the faculty at the IMDEA Software Institute in Madrid, Spain, since 2011. Previously, she obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign, from where she also obtained a masters in Applied Mathematics. She has a masters degree in Computer Science from the Indian Institute of Science, Bangalore and a bachelors degree from the National Institute of Technology, Warangal, in India. She spent the year between 2011-2012 at the California Institute of Technology as a CMI (Center for Mathematics of Information) fellow. Her main research interest is in Formal Analysis of Cyber-Physical Systems, more precisely, hybrid systems, with focus on both theoretical and practical aspects.

Galois is pleased to host the following tech talk. These talks are free and open to the interested public--please join us! (There is no need to pre-register for the talk.)

Abstract

EasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However, there is a significant gap between security proofs done in the usual provable security style and cryptographic implementations used in practice; as a consequence, real-world cryptography is sometimes considered as “one of the many ongoing disaster areas in security. We have recently extended EasyCrypt with support for reasoning about C implementations, and exploited the CompCert verified compiler to carry the security proof to executable code. Moreover, we have developed verified type-based information flow analyses on assembly code to ensure that executable code is protected against cache-based side-channel attacks.

Bio

Gilles Barthe received a Ph.D. in Mathematics from the University of Manchester, UK, in 1993, and an Habilitation à diriger les recherches in Computer Science from the University of Nice, France, in 2004. He joined the IMDEA Software Institute in April 2008. Previously, he was head of the Everest team on formal methods and security at INRIA Sophia-Antipolis Méditerranée, France. He also held positions at the University of Minho, Portugal; Chalmers University, Sweden; CWI, Netherlands; University of Nijmegen, Netherlands. He has published more than 100 refereed scientific papers. He has been coordinator/principal investigator of many national and European projects, and served as the scientific coordinator of the FP6 FET integrated project “MOBIUS: Mobility, Ubiquity and Security” for enabling proof-carrying code for Java on mobile devices (2005-2009). He has been a PC member of many conferences (CSF, ESORICS, FM, ICALP, ITP…), and served as PC (co-)chair of VMCAI’10, ESOP’11, FAST’11, and SEFM’11. He is a member of the editorial board of the Journal of Automated Reasoning.

His research interests include formal methods, programming languages and program verification, software and system security, and cryptography, and foundations of mathematics and computer science.

abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002. A similar mechanism was added to Sequent’s DYNIX/ptx parallel UNIX kernel in 1993, and antecedents go back to at least 1980. Although a fully functional textbook implementation of RCU comprises only about 20 lines of code, the Linux-kernel implementation comprises more than 15,000 lines of code due to harsh requirements involving performance, scalability, energy efficiency, real-time response, memory footprint, module unloading, hotplugging of CPUs, and software-engineering considerations.

Therefore, a key Linux-kernel RCU challenge is validation and verification. To this end, more than 2500 lines of the current Linux-kernel implementation do torture testing. However, there are now more than one billion devices running Linux, so that an RCU bug that manifested on average once every million years of machine time would manifest about three times every day across the installed base. Furthermore, the combination of Internet of Things and Josh Triplett’s Linux Kernel Tinification project is likely to significantly increase the number of running instances.

I write and run rcutorture tests myself, and I like to think that my 20 years of parallel-code testing experience allows me to meet this validation challenge, but a simple analysis suggests a gap of several orders of magnitude. Additional validation and verification techniques are thus called for. This talk gives a brief overview of RCU and describes my adventures evaluating various verification techniques.

bio: Paul E. McKenney has been coding for almost four decades, more than half of that on parallel hardware, where his work has earned him a reputation among some as a flaming heretic. Over the past decade, Paul has been an IBM Distinguished Engineer at the IBM Linux Technology Center. Paul maintains the RCU implementation within the Linux kernel, where the variety of workloads present highly entertaining performance, scalability, real-time response, and energy-efficiency challenges. Prior to that, he worked on the DYNIX/ptx kernel at Sequent, and prior to that on packet-radio and Internet protocols (but long before it was polite to mention Internet at cocktail parties), system administration, business applications, and real-time systems. He has a BS in Computer Science and another in Mechanical Engineering along with an MS in Computer Science, all from Oregon State University. He also has a Ph.D. in Computer Science and Engineering from OGI/OHSU. He has more than 100 publications and more than 50 patents. His hobbies include what passes for running at his age along with the usual house-wife-and-kids habit.

Title: New Applications of Software Synthesis: Firewall Repair and Verification of Configuration Files

Abstract: In this talk we present a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls – whether the policies in the firewalls meet the specifications of their administrators – is an important but challenging problem. In our approach, after an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behavior. Based on the given examples, we automatically synthesize new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behavior of the original firewall.

We also show, using verification for configuration files, how to learn specification when the given examples is actually a set of configuration files. Software failures resulting from configuration errors have become commonplace as modern software systems grow increasingly large and more complex. The lack of language constructs in configuration files, such as types and grammars, has directed the focus of a configuration file verification towards building post-failure error diagnosis tools. In this talk we describe a framework which analyzes data sets of correct configuration files and derives rules for building a language model from the given data set. The resulting language model can be used to verify new configuration files and detect errors in them.

Bio: Ruzica Piskac is an assistant professor (tenure-track) at Yale, Computer Science Department. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica's research is improving software reliability and trustworthiness using formal techniques. Ruzica has received a NSF CAREER award for her proposal, “Synthesis in a Live Programming Environment”. She proposed the concept of cooperative programming which combines a live programming environment and the programming by example paradigm.

Abstract: In this talk, I’ll give a high-level overview of Penn’s Vellvm (Verified LLVM) project, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results, in which we verified memory safety transformations and a variant of LLVM’s mem2reg optimization, focusing on the structure of the proof techniques. Along the way, I’ll highlight some of the challenges of reasoning about LLVM code (many of which are still open issues). I’ll wrap up with a status report about our ongoing efforts to re-engineer Vellvm as part of the DeepSpec NSF Expeditions project.

No experience with LLVM or Coq will be assumed.

Bio: I study programming languages and computer security. I have wide-ranging interests, and some of my most recent work touches on: Coq verification of LLVM program transformations and randomized algorithms, type-directed program synthesis, linear types and GUI programming. I have also spent a lot of time thinking about language-based enforcement of information-flow policies, low-level code memory safety, understanding dynamic security policies, and authorization logic. I am also interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory.

Abstract: Formal verification has become a well-established part of standard hardware design flows leveraging SAT solvers and model checkers for verification tasks including logical equivalence checking, property checking, and protocol verification. These tools are largely based on all-digital, synchronous, single clock-domain models of hardware behaviour. To address the needs of system-on-chip and multi-core designs, we are developing verification methods for asynchronous, analog, mixed-signal, and mixed-timing circuits.

A key enabling technology for our research is the integration of an SMT solver, Z3, into an interactive theorem prover, ACL2. Our integration, Smtlink, exploits ACL2’s extensive support for reflection: we can write lisp functions that operate on the syntax of pending goals by extracting facts (e.g. function definitions and previously proven theorems) from the ACL2 logical world. Smtlink can automatically translate high-level goals that include user-defined data types and recursive functions into formulas that are in the logic of the SMT solver. We demonstrate the efficacy of this approach with the verification of timed asynchronous handshake circuits and a convergence proof for a digital phase-locked loop.

I will briefly describe related verification work including using automatic differentiation (AD) based algorithms to reason about synchronizers and analog circuits, and interval-arithmetic based verification algorithms to reason about convergence properties of non-linear circuits. Currently, I am working with students and other faculty at UBC to explore verification challenges arising in operating system research, cyber-physical systems, and numerical optimization algorithms used for machine learning.

I gratefully acknowledge my collaborators including Chris Chen, Ian Jones, Matt Kaufmann, Carl Kwan, Yan Peng, Justin Reiher, Mark Schmidt, and Margo Seltzer.

Bio: Mark Greenstreet is a professor in the Department of Computer Science at the University of British Columbia. He earned his B.Sc. (1981) from Caltech, and his MA (1988) and Ph.D. (1992) from Princeton. His research interests span a wide range of formal verification topics, especially any problem, hardware or software, that involves concurrency and/or continuous models. Mark has industrial chip design experience spanning from a design of an FFT chip set for ESL (at TRW subsidiary) in the early 1980’s to work on verifying the synchronizers and clock-domain-crossing circuits in many generations of SPARC CPUs.