[cap-talk] Dan Bernstein's qmail security lessons paper

[Sandro Magi]

David Wagner wrote:
> That's not modular arithmetic.  Modular arithmetic would be
> 
>  val modplus: int -> int -> int
> 
> where modplus x y returns x+y mod 2^w, for some word size w.
> 
> I accept the similarities between "fixed-precision integer arithmetic
> with exception on overflow" and "unlimited-precision integer arithmetic
> with exception on resource exhaustion", but neither of those are
> modular arithmetic.

Sorry, I got my signals crossed. You are correct. When I made the
statement, I was considering the extreme, where the largest integer one
could conceivably operate on is limited by addressable memory, and thus
has modular semantics. For instance, keep an operand in a register and
destructively update all of memory holding the large integer.

The addition function I outlined does not wrap, but it does have a more
usable semantics. BigInt addition can be made to wrap, but the semantics
are undesirable. For instance, if only w bits are available, then
addition would wrap on 2^w. Yuck. Or allow more explicit resource
management with effectful semantics: clients preallocate an integer with
word size w and with the possibility of failure, then fill:

type Result = Exhausted | Success of PreInt
val new_sized : int -> Result
val (+) : int -> int -> PreInt -> int

You would need a linear type system to ensure that the PreInt cannot be
used after the addition. Actually, using linear types I think a more
usable semantics is possible, but you get the idea.

I'd be interested in more pleasant alternatives, as I think totality is
critical for writing correct software; the more total functions over
partial functions used, the fewer the failure modes, and the better
behaved the program.

Sandro