Liquid Haskell: Haskell as a theorem prover

Abstract

Code deficiencies and bugs constitute an unavoidable part of software systems. In safety critical systems, like aircrafts or medical equipment, even a single bug can lead to catastrophic impacts such as injuries or death. Formal verification can be used to statically track code deficiencies by proving or disproving correctness properties of a system. However, at its current state formal verification is a cumbersome process that is rarely used by mainstream developers, mostly because it targets non general purpose languages (e.g., Coq, Agda, Dafny).We present LIQUID HASKELL, a usable program verifier that aims to establish formal verification as an integral part of the development process. LIQUID HASKELL naturally integrates the specification of correctness properties as logical refinements of Haskell’s types. Moreover, it uses the abstract interpretation framework of liquid types to automatically check correctness of specifications via Satisfiability Modulo Theories (SMT) solvers requiring no explicit proofs or complicated annotations. Finally, the specification language is arbitrary expressive, allowing the user to write general correctness properties about their code, thus turning Haskell into a theoremprover. Transforming a mature language — with optimized libraries and highly tuned parallelism — into a theorem prover enables us to verify a wide variety of properties on real world applications. We used LIQUID HASKELL to verify shallow invariants of existing Haskell code, e.g. memory safety of the optimized string manipulation library ByteString. Moreover, we checked deep, sophisticated properties of parallel Haskell code, e.g. program equivalence of a naıve string matcher and its parallelized version. Having verified about 20K of Haskell code, we present how LIQUID HASKELL serves as a prototype verifier in a future where formal techniques will be used to facilitate, instead of hinder, software development.

Οι ελλείψεις στον κώδικα και τα σφάλματα αποτελούν αναπόφευκτο μέρος των λογισμικών συστημάτων. Σε συστήματα κρίσιμα για την ασφάλεια, όπως αυτά των αεροσκαφών ή του ιατρικού εξοπλισμού, ακόμα και ένα μόνο σφάλμα μπορεί να οδηγήσει σε καταστροφικές συνέπειες, όπως τραυματισμούς ή θάνατο. Η τυπική επαλήθευση μπορεί να χρησιμοποιηθεί για τον στατικό εντοπισμό ελλείψεων στον κώδικα, αποδεικνύοντας ή διαψεύδοντας ιδιότητες ορθότητας ενός συστήματος. Ωστόσο, στην παρούσα της μορφή, η τυπική επαλήθευση είναι μια περίπλοκη διαδικασία που σπάνια χρησιμοποιείται από προγραμματιστές του ευρύτερου χώρου, κυρίως επειδή αφορά γλώσσες που δεν είναι γενικού σκοπού (π.χ. Coq, Agda, Dafny). Παρουσιάζουμε το LIQUID HASKELL, έναν πρακτικό επαληθευτή προγραμμάτων που στοχεύει στην καθιέρωση της τυπικής επαλήθευσης ως αναπόσπαστο μέρος της διαδικασίας ανάπτυξης λογισμικού. Το LIQUID HASKELL ενσωματώνει φυσικά τον καθορισμό ιδιοτήτων ορθότητας ως λογικές εξειδικεύσεις στους τύπους της Haskell. Επιπλέον, χρησιμοποιεί το πλαίσιο αφηρημένης ερμηνείας των “liquid types” ώστε να ελέγχει αυτόματα την ορθότητα των προδιαγραφών μέσω επιλυτών SMT (Satisfiability Modulo Theories), χωρίς να απαιτούνται ρητές αποδείξεις ή περίπλοκες επισημάνσεις. Τέλος, η γλώσσα προδιαγραφής είναι αυθαίρετα εκφραστική, επιτρέποντας στον χρήστη να γράφει γενικές ιδιότητες ορθότητας για τον κώδικά του, μετατρέποντας έτσι τη Haskell σε αποδεικτικό εργαλείο θεωρημάτων. Η μετατροπή μιας ώριμης γλώσσας — με βελτιστοποιημένες βιβλιοθήκες και ιδιαίτερα αποδοτική παραλληλοποίηση — σε αποδεικτικό εργαλείο, μας επιτρέπει να επαληθεύσουμε ευρύ φάσμα ιδιοτήτων σε εφαρμογές πραγματικού κόσμου. Χρησιμοποιήσαμε το LIQUID HASKELL για να επαληθεύσουμε ρηχές ακεραιότητες σε υπάρχοντα Haskell προγράμματα, π.χ. την ασφάλεια μνήμης της βελτιστοποιημένης βιβλιοθήκης επεξεργασίας συμβολοσειρών ByteString. Επιπλέον, ελέγξαμε βαθιές και σύνθετες ιδιότητες παραλληλισμένου Haskell κώδικα, π.χ. την ισοδυναμία ενός απλού αλγορίθμου εύρεσης συμβολοσειράς και της παραλληλοποιημένης εκδοχής του. Έχοντας επαληθεύσει περίπου 20.000 γραμμές Haskell κώδικα, παρουσιάζουμε πώς το LIQUID HASKELL λειτουργεί ως ένας πρωτότυπος επαληθευτής σε ένα μέλλον όπου οι τυπικές τεχνικές θα διευκολύνουν — αντί να εμποδίζουν — την ανάπτυξη λογισμικού.