Home » forums » LtU Forum

An experiment: Refined types - a better type system for more secure software

Hi, fellow language enthusiasts!

I recently finished an experimental, fairly simple, OCaml implementation of refined types. Refined types support logical predicates in function parameters and return types, for example:

/ : (int, i : int if i != 0) -> int

random1toN : (N : int if N >= 1) -> (i : int if 1 <= i and i <= N)

length : forall[t] (a : array[t]) -> (l : int if l >= 0)

get : forall[t] (a : array[t], i : int if i >= 0 and i < length(a)) -> t

Refined types are checked by an external automatic theorem prover (Z3), and can prevent many common software errors, such as division by zero and out-of-bounds array access. Given correct refined types on functions alloc and memcpy, they could even be used to prevent Heartbleed bug!

Read more about it (and see the code) here! Any comments are welcome.

By Tom Primožič at 2014-05-29 11:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 3929 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Refinement and Dependent

I'm not too familiar with where the lines are drawn, but these examples of refinement types seem to be less expressive/powerful than dependent typing for at least two reasons:

  • Inability to mix type-level and data-level expressions (other than in predicates)
  • Due to how predicates work, going from data-level to type-level loses potentially important information (as it gets cast to a type-level boolean)

Are these restrictions the case? It may be that these restrictions make refinement easier to learn than dependent typing, so it is not just an issue of expressiveness.

Additionally, does Z3 check the refinement types at run time like higher-order contracts or are they checked at compile time?

By kms at Thu, 2014-05-29 13:51 | login or register to post comments

I've not researched or

I've not researched or though about mixing data-level and type-level expressions other that with predicates (e.g. having array[int, 5]), but I imagine an equivalent type could be modeled as array[int] if length(array) == 5.

Having said that, refined types (types with predicates) are almost certainly not as powerful as full dependent types, at least not as presented in the sources I've read. Usually HM type inference is performed first, and contracts just annotate HM types, so there can be no e.g. dependent sums such as having a tuple with \(n\) int elements (but you can have an array with \(n\) elements). Nevertheless, they appear quite useful.

Z3 is only invoked at compile time. Depending on an implementation strategy, if it could neither show a contract could be broken nor prove that it cannot be broken, the compiler could either reject the program and require more proof from the programmer, or compile the program with runtime checks, which would not require Z3 (as they are just the compiled contract expressions). The latter was described in papers [1] and [2].

[1] K Knowles, C Flanagan. Hybrid Type Checking [pdf]. 2006/2010

[2] K Knowles, A Tomb, J Gronski, S N Freund, C Flanagan. Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic [pdf]. 2006

By Tom Primožič at Thu, 2014-05-29 15:06 | login or register to post comments