John Harrison wrote:
> * Each type constructor has an int for its arity and when the user
> tries to construct a type with it, this value is compared with the
> length (also as an int) of the list of type arguments. So in
> principle you could declare a type constructor with arity n and
> later give it n + 2^31 arguments (on a 32-bit platform). This is
> a bit of a rough edge, but of somewhat academic interest, and I
> don't think it implies a soundness problem (you could imagine
> allowing type constructors with the same name but different
> arities). Still, maybe Mark Adams will find a flaw in that
> reasoning and then I'll change to using unit list instead of int!
You've got me worried now. This use of integers could be exploited when
defining a new type operator. In general, the input theorem to type
operator definition is:
|- ?x. P x or in HOL Light as |- P x
Imagine the type of 'x' is, say, cartesian product with 2^31 dimensions and
a type variable for each dimension, and 'P' is, say, `\x. true`. Then the
resulting type operator will be given arity 0 (because the OCaml int length
of the list of type variables will be 2^31, which wraps round as 0 in
OCaml), and the theorem that defines it will state that this 0-dimensioned
type constant is in bijection with the the entire 2^31-dimensioned
representation type (with its 2^31 type parameters). Inconsistency should
be derivable by using two different type instantiations of this definition
theorem.
HOL Zero is just as vulnerable as HOL Light here, because it also used
OCaml's int for type arities.
I always thought that this would be impossible to exploit in practice, but
now I'm thinking 2^31 =~ 2 billion, and this is perhaps doable in principle
with a machine with something like 100 GB of RAM (although inefficiencies in
the 'union' operation used to compile a term's type variables would mean the
execution would surely take years).
Does this mean unit lists in HOL Light? :)
I'm thinking of adding a check that there are no more than 2^30-1 type
variables in the input theorem.
Mark.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
