UC3 - Verificação Formal

Programa Resumido

• Lógica e Sistemas de Prova
  • Sistemas de prova automática:
    • lógica proposicional; SAT solvers;
    • lógica de 1ª ordem; teorias de 1ª ordem; SMT solvers.
  • Sistemas de prova assistida:
    • lógica de ordem superior; the Coq proof assistant.

• Verificação de Software
  • Verificação dedutiva de programas:
    • lógica de Hoare; VCGen; safety verification; functional verification;
    • a plataforma Why3 para verificação dedutiva de programas;
    • anotações em ACSL; o plug-in WP da ferramenta Frama-C.
  • Verificação automática de programas:
    • bounded model checking of software; CBMC.

Material de Apoio

Slides

• Introduction
• Propositional Logic & SAT solvers
• First-Order Logic & Theories
• SMT solvers
• Deductive Reasoning & the Coq Proof Assistant
• Inductive Reasoning in Coq
• Programming and Proving in Coq
• Deductive Program Verification
• Deductive Program Verification with Why3 (JC Filiatre)
• Deductive Program Verification with Frama-C
• Introduction to CBMC (Arie Gurfinkel)
• CBMC by example

Guiões

• Guião 1: SAT solving -- Ficheiros para a aula
• Guião 2: SMT solving -- Ficheiros para a aula
• Guião 3: Coq (1) -- Ficheiros para a aula
• Guião 4: Coq (2) -- Ficheiros para a aula
• Guião 5: Coq (3) -- Ficheiros para a aula
• Guião 6: Why3 (1) -- Ficheiros para a aula
• Guião 7: Why3 (2) -- Ficheiros para a aula
• Guião 8: Frama-C (1) -- Ficheiros para a aula
• Guião 9: Frama-C (2) -- Ficheiros para a aula
• Guião 10: CBMC -- Ficheiros para a aula

Ferramentas

Uma parte substancial do software listado é desenvolvido em Ocaml, uma linguagem funcional da família ML, e pode ser compilado localmente. Recomenda-se a instalação do package manager OPAM (disponível em Homebrew para Max OSX).

• SAT Live! - keep up to date with research on the satisfiability problem
  • List of SAT solvers
  • Recomendado instalar: MiniSat (disponível em Homebrew para Max OSX)
  • MiniSat user guide

• SMT-LIB - The Satisfiability Modulo Theories Library
  • Solvers recomendados:
    • Z3 (disponível no Homebrew para Max OSX)
    • CVC4 (disponível Cask no Homebrew para Max OSX)
    • Yices2 (disponível no Homebrew para Max OSX)
    • Alt-ergo (disponível no Opam)
  • Documentação

• The Coq Proof Assistant (disponível no Opam)
  • Recomendado instalar: CoqIde (disponível no Opam)
  • Documentação

• Why3: Where Programs Meet Provers (disponível no Opam)
  • Versão online
  • Documentação

• Frama-C - Software Analyzers (disponível no Opam)
  • Documentação
  • Wiki
  • Em particular:
    • ACSL by example
    • ACSL tutorial
    • ACSL reference manual

• CBMC - A Bounded Model Checker for C and C++ programs.

Máquina virtual com todas as ferramentas instaladas.

• Software instalado
• Instalação de ferramentas do Frama-C (Switch Opam)

Bibliografia

• Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
• The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
• Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011)
• Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Yves Bertot & Pierre Casteran. Springer (2004)

Funcionamento

Docente / Horário

Docente	Foto	Horário	Sala
Maria João Frade		5a-feira, 14h-17h	Sala E7 1.10

NB: poderá haver trocas de horário entre VF e AC de acordo com necessidades de serviço dos docentes das duas disciplinas.

Avaliação

• 2 testes, com nota mínima (agregada) de 8 valores (70%)
• 1 trabalho desenvolvido em grupo, envolvendo o estudo de um tópico (diferente para cada grupo), e possivelmente algum desenvolvimento. O trabalho deverá dar origem a um artigo a entregar no final do semestre, bem como a uma apresentação feita por todo o grupo (30%)

• Datas
  • 1º teste: 4 de Abril (9:00)
  • 2º teste: 30 de Maio (14:00)
  • Projecto
    • Relatório: 10 de Junho
    • Apresentação: 12 de Junho (9:00)
  • Exame de recurso: 19 Junho (14:00)

Projectos

Lean

“Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.”
Tratando-se de uma ferramenta de prova inovadora, e não de um verificador de programas, espera-se:

• uma descrição geral da ferramenta e princípios subjacentes;
• referência às vantagens que possa oferecer relativamente à utilização das ferramentas existentes bem estabelecidas;
• demonstração com base em exemplos abordados nesta UC, nomeadamente de provas com utilização de indução.

Isabelle

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
Tratando-se de uma ferramenta de prova, e não de um verificador de programas, espera-se:

• uma descrição geral da ferramenta e princípios subjacentes;
• referência às vantagens que possa oferecer relativamente à utilização das ferramentas existentes bem estabelecidas;
• demonstração com base em exemplos abordados nesta UC, nomeadamente de provas com utilização de indução.

Coq

"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs." Tratando-se de uma ferramenta de prova que já foi abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:

• desenvolvimento de um caso de estudo que envolva a formalização em Coq de um pequeno problema;
• consideração de alguns tópicos avançados, não abordados nas aulas (por exemplo, definição de tácticas automáticas);
• experimentação com a ferramenta QuickChick: Randomized Property-Based Testing Plugin for Coq.

Why3

"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories and basic programming data structures. A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 can be easily extended with support for new theorem provers. Why3 can be used as a software library, through an OCaml API." Tratando-se de uma ferramenta já abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:

• desenvolvimento de um caso de estudo que envolva a formalização em Why3 de um pequeno problema (ver aqui);
• comparação com as ferramentas similares;
• consideração de tópicos avançados: linguagem lógica / tipos indutivos / ghost code.

Boogie

"Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#. Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3. The Boogie research project is being developed at Microsoft Research."
Espera-se:

• tutorial sobre a utilização da ferramenta;
• comparação com a ferramenta Why3;
• consideração de tópicos avançados: linguagem lógica / tipos indutivos / ghost code.

Dafny

Dafny é uma ferramenta da Microsoft Research baseada numa linguagem de programação dedicada para verificação dedutiva (tal como Why3), utilizando como VCGen uma outra ferramenta da Microsoft Research, chamada Boogie.
Espera-se:

• tutorial sobre a utilização da ferramenta;
• comparação com as ferramentas similares estudadas na UC (WP e Why3);
• consideração de tópicos avançados: linguagem lógica / tipos indutivos / ghost code.

The KeY Project

O KeY é uma ferramenta de verificação dedutiva bem estabelecida que ganhou recentemente visibilidade acrescida, pelo facto de ter permitido identificar um bug em algoritmos de ordenação implementados em bibliotecas standard (Java, Python). A lógica de programas subjacente é uma lógica dinâmica, em vez da mais comum lógica de Hoare / WP calculus.
Espera-se:

• tutorial sobre a utilização da ferramenta;
• comparação com as ferramentas similares estudadas na UC (WP e Why3);
• consideração de tópicos avançados: linguagem lógica / tipos indutivos / ghost code.

VeriFast

O VeriFast é uma ferramenta de verificação dedutiva tendo por base a lógica de programas conhecida como “separation logic”, o que, em teoria, lhe confere algumas vantagens sobre ferramentas baseadas em lógica de Hoare / WP calculus.
“VeriFast is a research prototype of a tool for modular formal verification of correctness properties of single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.”
Espera-se:

• tutorial sobre a utilização da ferramenta;
• comparação com as ferramentas similares estudadas na UC (WP e Why3);
• identificação de aspectos em que a ferramenta suplanta as estudadas, graças à utilização de “separation logic”;
• consideração de tópicos avançados: linguagem lógica / tipos indutivos / ghost code.

Viper

“Viper (Verification Infrastructure for Permission-based Reasoning) is a suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. It comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages, via translations into the Viper language.
The Viper toolchain is designed to make it easy to implement verification techniques for programs with persistent mutable state (including concurrent programs), providing native support for reasoning about the program state using method permissions or ownership, e.g. in the style of separation logic. New verification techniques can be implemented directly as translations to the Viper language, using either of the verifiers provided.”
Trata-se de uma proposta completa, baseada numa linguagem intermédia, front-ends e back-ends. São disponibilizados dois back-ends, um dos quais recorre ao Boogie.
Espera-se naturalmente uma descrição geral da toolset e princípios subjacentes, abordando:

• uma comparação entre a linguagem intermédia dedicada Wiper e a linguagem WhyML do Why3;
• comparação entre Viper e Why3, trabalhando directamente sobre as respectivas linguagens dedicadas;
• possível demonstração da utilização do toolset, incluindo um front-end para uma qualquer linguagem real de alto nível.

SMACK

“SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. SMACK handles complicated feature of the C language, including dynamic memory allocation, pointer arithmetic, and bitwise operations.
(…) Currently, SMACK leverages the Boogie and Corral verifiers.”
Trata-se de uma ferramenta para a verificação de código C, mas que apenas traduz para BoogiePL, sendo depois necessário utilizar uma das ferramentas referidas como back-end. O grupo deve começar por escolher uma das ferramentas; o trabalho diz respeito ao toolset completo, compreendendo o SMACK e a ferramenta (VCGen) escolhida.
Espera-se:

• uma descrição geral da toolset e princípios subjacentes;
• referência às vantagens que possa oferecer relativamente à utilização de outras ferramentas existentes para a verificação de código C;
• comparação com as ferramentas similares estudadas na UC (WP / Frama-C).

Distribuição dos projectos