Semantics and proof calculus for communicating unstructured code

Abstract

Software becomes ever more ubiquitous and complex. Its use in safety-critical environments, where errors may harm people or cost great amounts of money, requires a high level of con dence in its correctness. In order to ensure such levels of con- dence, the use of formal veri cation methods to prove properties of the systems is an important tool. Such formal methods are widely applied to verify hardware and software, the latter usually written or modelled in high-level languages which are much easier to reason about. Such languages are, however, very di erent from the machine code which is actually executed. Therefore, the formalization of unstructured code may be necessary for some applications, such as the veri cation of compilers. Formal veri cation of sequential, structured programs has been extensively explored, but the techniques for concurrent or unstructured code are still an open problem. Furthermore, most approaches contemplate either concurrency and communication or unstructured code, not supporting the combination of the two. In this thesis, operational semantics in small- and big-step style and a proof calculus are de ned for Low-Level Do (LLDo), a small and exible unstructured language for communicating processes which should be general enough to model more complex languages. The big-step semantics and the proof calculus are de ned in a compositional way, unifying techniques already used for dealing with communicating or unstructured code individually. The applicability of the calculus is tested on some simple examples.

Software tende a se tornar cada vez mais onipresente e complexo. Seu uso em aplicações críticas, onde defeitos podem causar grandes danos materiais, ambientais ou até mortes, exige um alto grau de confiança em sua corretude. Para garantir tais níveis de confiança, a verificação formal é uma boa ferramenta, dado que pode provar propriedades do sistema ou de seus modelos. Métodos formais já são frequentemente empregados na verificação de hardware e software, sendo o software normalmente implementado ou modelado em linguagens com alto nível de abstração, cuja análise é mais simples. Tais linguagens são, no entanto, bastante diferentes do código de máquina que é efetivamente executado. A formalização de código não-estruturado pode, portanto, ser necessária para algumas aplicações, como a verificação de compiladores. Enquanto a verificação de programas sequenciais e estruturados já foi extensivamente explorada, programas concorrentes ou não-estruturados ainda são um problema em aberto. Além disso, a maioria das abordagens existentes lida apenas com um dos dois aspectos, e não com a sua combinação. Neste trabalho é definida uma semântica formal para a linguagem Low-Level Do (LLDO), uma linguagem não-estruturada pequena e flexível que permite a especificação de processos comunicantes. A semântica operacional é apresentada tanto em estilo Small-Step quanto Big-Step. Além disso, um cálculo é proposto para a verificação de corretude de tais programas. Tanto a semântica Big-Step quanto o cálculo são definidos de maneira composicional ao combinar técnicas existentes que lidam individualmente com concorrência ou código não-estruturado. A aplicabilidade do cálculo é testada em alguns exemplos, e todo o trabalho é formalizado no assistente de provas Isabelle/HOL.

Die Korrektheit von Software ist besonders bei sicherheitskritischen Anwendungen von entscheidender Bedeutung, wenn Fehler das Leben von Menschen gefahrden konnen oder gro en nanziellen Schaden anrichten. Um die Korrektheit sicherzustellen, sind formale Veri kationsverfahren wichtig, da sie Eigenschaften der Systeme mathematisch beweisen konnen. Fur die Veri kation von Programmen, die in hoheren, strukturierten Programmiersprachen geschrieben wurden, werden diese Verfahren schon hau g in der Praxis angewendet. Strukturierte Programmiersprachen unterscheiden sich allerdings sehr von unstrukturiertem Maschinencode, in den sie ubersetzt werden und der anschlie end tatsachlich durchgefuhrt wird. Die Formalisierung unstrukturierter Sprachen ist also in gewissen Fallen notwendig, beispielsweise fur die Veri kation von Compilern. Obwohl einige Verfahren fur die Veri kation von unstrukturiertem Code schon existieren und weitere fur nebenlau- ge, kommunizierende Programme, konnen sie mit beiden Eigenschaften umgehen. In dieser Arbeit wird eine operationale Semantik im Small-Step- und Big-Step- Stil sowie ein Korrektheitskalkul fur Low-Level Do (LLDo) entwickelt. LLDo ist eine kleine, exible und unstrukturierte Programmiersprache, die nebenlau ge und kommunizierende Prozesse beschreibt. Um unstrukturierte und kommunizierende Programme kompositional behandeln zu konnen, werden existierende Ansatze fur die jeweiligen Problemstellungen kombiniert. Die Anwendbarkeit des Kalkuls wird mit einigen einfachen Beispielen gezeigt.