Dependent Types for Low-Level Programming

Dependent Types for Low-Level Programming by Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula:

In this paper, we describe the key principles of a dependent type system for low-level imperative languages. The major contributions of this work are (1) a sound type system that combines dependent types and mutation for variables and for heap-allocated structures in a more flexible way than before and (2) a technique for automatically inferring dependent types for local variables. We have applied these general principles to design Deputy, a dependent type system for C that allows the user to describe bounded pointers and tagged unions. Deputy has been used to annotate and check a number of real-world C programs.

A conceptually simple approach to verifying the safety of C programs, which proceeeds in 3 phases: 1. infer locals that hold pointer bounds, 2. flow-insensitive checking introduces runtime assertions using these locals, 3. flow-sensitive optimization that removes the assertions that it can prove always hold.

You're left with a program that ensures runtime safety with as few runtime checks as possible, and the resulting C program is compiled with gcc which can perform its own optimizations.

This work is from 2007, and the project grew into the Ivy language, which is a C dialect that is fully backwards compatible with C if you #include a small header file that includes the extensions.

It's application to C probably won't get much uptake at this point, but I can see this as a useful compiler plugin to verify unsafe Rust code.

By naasking at 2015-09-28 13:58 | Theory | Type Theory | other blogs | 24810 reads

dependent types and effects

I think it is also an interesting design point when considering how to integrate dependent types with effects and mutable states. Nowadays this is a fashionable topic, with languages like Ynot and F-star. But here is a much more low-tech and unambitious alternative: you just pick some sublanguage of pure expressions, and make types depend on those only. That approach will not let you prove any interesting theorems about effectful code, but as this paper shows, it can still be useful for reasoning about the pure part (to make sure that array indices are in bounds).

You could imagine taking this even further, by mashing together C and Agda. That is, expand the C expression syntax to have

exp ::= ... | agda_expression

and then write the things that must be fast in C and the things that must be safe in Agda... :)

By Vilhelm Sjoberg at Mon, 2015-09-28 14:46 | login or register to post comments

How do you ensure that

How do you ensure that well-typed code can't go wrong, if C and Agda interoperate? If you don't, is this still worthwhile?
Think of the problems addressed by gradual typing: well-typed code can trigger type errors if the untyped (or weakly typed) code gives it invalid data. So you can take lots of time to write safe Agda, only to run into errors at the interface.

Or am I missing something, or somehow worrying too much?

By Blaisorblade at Mon, 2015-09-28 18:05 | login or register to post comments

missing pdf link

http://www.cs.berkeley.edu/~necula/Papers/deputy-tr-2006.pdf

By Kartik Agaram at Mon, 2015-09-28 20:32 | login or register to post comments

There is also: CSolve Liquid Types-Based C Program Verifier

Here is another gem that tries to verify C with a refinement type system.

http://goto.ucsd.edu/csolve/

CSolve
Liquid Types-Based C Program Verifier

CSolve is a Liquid Types-based verifier for C programs which can verify sophisticated program properties like memory safety, deterministic parallel execution, and invariants of linked data structures, while imposing an extremely low annotation overhead on the programmer.

By HeikoWengler at Tue, 2015-09-29 08:13 | login or register to post comments

Liquid vs Dependent

What is the difference between a dependent and a liquid type?

By Keean Schupke at Tue, 2015-09-29 09:08 | login or register to post comments

I am not a type theorist...

I am not a type theorist... from

Liquid Types (PLDI 2008) http://goto.ucsd.edu/~pmr/papers/liquid-types-pldi08.pdf

Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala
:
"... Logically Qualified Data Types, abbreviated to Liquid Types
, a system that combines Hindley-Milner type inference with
Predicate Abstraction to automatically infer dependent types pre-
cise enough to prove a variety of safety properties. Liquid types
allow programmers to reap many of the benefits of dependent
types, namely static verification of critical properties and the elim-
ination of expensive run-time checks, without the heavy price of
manual annotation."

By HeikoWengler at Tue, 2015-09-29 18:28 | login or register to post comments

Liquid types are dependent types?

So it looks like liquid types are in fact dependent types plus a way of applying HM style type inference to avoid having to annotate everything with its type. Sounds quite nice.

By Keean Schupke at Wed, 2015-09-30 05:56 | login or register to post comments

That's my understanding

That's my understanding too.
And better: They implemented it for C, ocaml and Haskell.
csolve can prove memory safety and thread safety of c programs.

By HeikoWengler at Wed, 2015-09-30 08:18 | login or register to post comments

Typing 'C'

I'm intersected because a type system that can type 'C' can act as a type system internal to the compiler for all the stages of compilation. I had a big problem with dependent types for a long time because I could not work out how to stratify them to track what can be partialy evaluated in the type system. Recently I have realised that information can be carried in a monad,

By Keean Schupke at Wed, 2015-09-30 10:49 | login or register to post comments

as seen

previously on ltu.

By raould at Wed, 2015-09-30 21:07 | login or register to post comments

except

Except now with software and a working link. ;)

By NickP at Wed, 2015-10-14 01:18 | login or register to post comments

thanks

I saw the old paper but now a link and software to try? Why thank you! :)

By NickP at Wed, 2015-10-14 01:18 | login or register to post comments

Admin category?

It seems like this post is in the wrong category.

By Andrew Moss at Tue, 2015-09-29 09:06 | login or register to post comments

good stuff

I'm glad you posted it. I've mainly been looking at Softbound + CETS (or hardware stuff) for C as I thought it was the next step from CCured. Such tools are also quite productive. :) Have no idea how I missed Ivy, esp with their Linux kernel work. Had to hit Archive.org on many PDF's but worth it. Good stuff with a lot of potential given the time they put in vs benefits received. In theory, could mix their approach with others where heavyweight stuff protected what was "trusted" in their scheme.

Anyway, I think all of this still has potential outside of Rust. Some of us still hate C but need it for some legacy or low-level code. Improving that is an obvious benefit. However, remember that a private party can always pick up and improve a BSD/Linux/major-c-lib with nifty work like Ivy for special-purpose devices. The easier the assurance activity is, the more likely someone will do it. Especially if it won't break the codebase.

By NickP at Wed, 2015-10-14 01:15 | login or register to post comments

Deputy was done in the

Deputy was done in the TinyOS context... https://en.wikipedia.org/wiki/TinyOS

C sucks, but if you have to use it deputy, csolve, ccured, all the llvm based projects (too many to write them down) are really helpful.
Especially in the IoT context...

Otherwise: Why not use ATS, rust, ocaml or even Ada to break free from C?

Heiko

By HeikoWengler at Wed, 2015-10-14 09:19 | login or register to post comments

Another hint:

Another hint: http://ssrg.nicta.com.au/projects/TS/autocorres/

AutoCorres : Automatic Specification Abstraction

AutoCorres is a research project of the Trustworthy Systems project inside the Software System Research Group (SSRG).
Spec chain
C code is automatically abstracted into increasingly more abstract specifications, easing manual reasoning about the code.

Aim: Simplify formal verification of C code by automatically and provably abstracting low-level C semantics into higher-level representations.

Overview: Before source code can be formally reasoned about, it must first be translated into the logic of a theorem prover. For example, to prove properties about C source code using the Isabelle/HOL theorem prover, a tool would be required to first convert the C into Isabelle/HOL, such as NICTA's C-to-Isabelle parser.

Active project used to prove operating system kernels in the IoT context.

By HeikoWengler at Fri, 2015-10-16 07:59 | login or register to post comments

Lambda the Ultimate

User login

Navigation