Malecha, Gregory Michael

Person:
Malecha, Gregory Michael

Last Name

Malecha

First Name

Gregory Michael

Name

Malecha, Gregory Michael

Full item page

Search Results

Now showing 1 - 8 of 8

Compositional Computational Reflection
(Springer Science + Business Media, 2014) Malecha, Gregory Michael; Chlipala, Adam; Baibant, Thomas
Current work on computational reflection is single-minded; each reflective procedure is written with a specific application or scope in mind. Composition of these reflective procedures is done by a proof- generating tactic language such as Ltac. This composition, however, comes at the cost of both larger proof terms and redundant preprocessing. In this work, we propose a methodology for writing composable reflective procedures that solve many small tasks in a single invocation. The key technical insights are techniques for reasoning semantically about extensible syntax in intensional type theory. Our techniques make it possible to compose sound procedures and write generic procedures parametrized by lemmas mimicking Coq’s support for hint databases.
Extensible Proof Engineering in Intensional Type Theory
(2015-02-24) Malecha, Gregory Michael; Morrisett, Greg; Chlipala, Adam; Chong, Stephen
We increasingly rely on large, complex systems in our daily lives---from the computers that park our cars to the medical devices that regulate insulin levels to the servers that store our personal information in the cloud. As these systems grow, they become too complex for a person to understand, yet it is essential that they are correct. Proof assistants are tools that let us specify properties about complex systems and build, maintain, and check proofs of these properties in a rigorous way. Proof assistants achieve this level of rigor for a wide range of properties by requiring detailed certificates (proofs) that can be easily checked. In this dissertation, I describe a technique for compositionally building extensible automation within a foundational proof assistant for intensional type theory. My technique builds on computational reflection---where properties are checked by verified programs---which effectively bridges the gap between the low-level reasoning that is native to the proof assistant and the interesting, high-level properties of real systems. Building automation within a proof assistant provides a rigorous foundation that makes it possible to compose and extend the automation with other tools (including humans). However, previous approaches require using low-level proofs to compose different automation which limits scalability. My techniques allow for reasoning at a higher level about composing automation, which enables more scalable reflective reasoning. I demonstrate these techniques through a series of case studies centered around tasks in program verification.
A More Precise Security Type System for Dynamic Security Tests
(2010) Malecha, Gregory Michael; Chong, Stephen
The move toward publically available services that store private information has increased the importance of tracking information flow in applications. For example, network systems that store credit-card transactions and medical records must be assured to maintain the confidentiality and integrity of this information. One way to ensure this is to use a language that supports static reasoning about information flow in the type system. While useful in practice, current type systems for checking information flow are imprecise, unnecessarily rejecting safe programs. This annoys programmers and often results in increased code complexity in order to work around these artificial limitations. In this work, we present a new type system for statically checking information flow properties of imperative programs with exceptions. Our key insight is to propagate a context of exception handlers and check exceptions at the throw point rather than propagating exceptions outward and checking them at the catch sites. We prove that our type system guarantees the standard non-interference condition and that it is strictly more permissive than the existing type system for Jif, a language that extends the Java type system to reason about information flow.
Preliminary Design of the SAFE Platform
(Association for Computing Machinery, 2011) Morrisett, Greg Gregory; DeHon, André; Karel, Ben; Malecha, Gregory Michael; Montagu, Benoît; Morisset, Robin; Pierce, Benjamin C.; Pollack, Randy; Ray, Sumit; Shivers, Olin; Smith, Jonathan M.; Sullivan, Gregory; Knight, Thomas F., Jr.
SAFE is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assembled a set of basic architectural choices that we believe will yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.
Mechanized Verification with Sharing
(Springer Verlag, 2010) Malecha, Gregory Michael; Morrisett, Greg Gregory
We consider software verification of imperative programs by theorem proving in higher-order separation logic. Separation logic is quite effective for reasoning about tree-like data structures, but less so for data structures with more complex sharing patterns. This problem is compounded by some higher-order patterns, such as stateful iterators and visitors, where multiple clients need to share references into a data structure. We show how both styles of sharing can be achieved without sacrificing abstraction using mechanized reasoning about fractional permissions in Hoare Type Theory.
Certified Web Services in Ynot
(2010-04-21) Wisnesky, Ryan; Malecha, Gregory Michael; Morrisett, Greg Gregory
In this paper we demonstrate that it is possible to implement certi ed web systems in a way not much di erent from writing Standard ML or Haskell code, including use of imperative features like pointers, les, and socket I/O. We present a web-based course gradebook application developed with Ynot, a Coq library for certi ed imperative programming.We add a dialog-based I/O system to Ynot, and we extend Ynot's underlying Hoare logic with event traces to reason about I/O be- havior. Expressive abstractions allow the modular certi cation of both high level speci cations like privacy guarantees and low level properties like memory safety and correct parsing.
Toward a verified relational database management system
(Association for Computing Machinery, 2010) Malecha, Gregory Michael; Morrisett, Greg Gregory; Shinnar, Avraham Ever; Wisnesky, Ryan
We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations that are proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for (finite) relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.
Effective Interactive Proofs for Higher-Order Imperative Programs
(Association for Computing Machinery, 2009) Chlipala, Adam; Malecha, Gregory Michael; Morrisett, Greg Gregory; Shinnar, Avraham Ever; Wisnesky, Ryan
We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules. We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.