Progress at last

This afternoon, I finally managed to get InforML to acceptably process one of my key examples. You start by defining some abstract data type

# Simple module defining an abstract datatype for rational numbers

module rational : sig
label Rat

type rat : (Lab -> * @ Rat) @

fun fromInt : 〈l:Lab〉 ((Int @ l) -(l)-> (rat @ l)) @

# Approximates to the nearest integer
fun toInt : ((rat @ ) -()-> (Int @ )) @

end = mod

newlabel Rat

type rat : (Lab -> * @ Rat) @ = (fn l:Lab => (Int @ l, Int @ l) end)

fun fromInt : 〈l:Lab〉 ((Int @ l) -(l)-> (rat @ l)) @
fun fromInt 〈l:Lab〉 (i : Int @ l) : rat @ l = (i, 1)

# Notice this is a more general type than the one
# exposed by the signature
fun toInt : 〈l:Lab〉 ((rat @ l) -(l)-> (Int @ l)) @
fun toInt 〈l:Lab〉 ((i1, i2) : rat @ l) : Int @ l = i1 div i2


The important thing to note here is that the abstraction assumes the invariant that the second integer in the pair will never become zero. Next you define a malicious function using type analysis

fun badtcase : 〈l:Lab (a:* @ l)〉 l <: info a => (a -(l)-> a) @
fun badtcase 〈p:Lab (b:* @ p)〉 (x:b) : b =
typecase b
of (Int @ p, Int @ p) => (1,0)
| _ => (x : b)

Now you use your malicious function to create an invalid instance of the abstract data type

val x = badtcase (rational.fromInt 42);
val x : (rational.rat @ rational.Rat)

And finally notice that this new corrupted value of the abstract data type cannot be used to cause a divide by zero, as

val _ = rational.toInt x

has an information content of rational.Rat which is greater than as specified by the signature.

Yes, I know that WordPress obliterated my whitespace, but I don't really feel like trying to fix it by hand at the moment. It also seems to enjoy converting all my <div> tags into <p> tags.

Leave a Comment