On Sun, 2007-01-28 at 12:30 -0800, Mark S. Miller wrote:
> Mark S. Miller wrote:
> > Oops, I get it. My mistake. If a module discharges its proof obligation,
> > then,
> > to my mind, it's just "free"ing, not "unsafe-free"ing. I should have made
> > this
> > clear.
>
> Other examples of the same principle:
>
> * An unprivileged module could be allowed to introduce secret static mutable
> state, for example, for use as a memoizing cache, if accompanied by a proof
> that this mutability has no overtly observable effects.
Yes.
> * We could allow a non-bounds-checked array store if accompanied by a proof
> that it would be within bounds. (Lacking an integrated proof system, Emily
> had
> to simply prohibit OCaml's Array.unsafe_set.)
Yes. Actually, this can mostly be done in the compiler today.
> * We could even allow the loading of arbitrary assembly code, if accompanied
> by a proof that all its observable effects were equivalent to an unprivileged
> BitC program that would have been accepted.
Or even a simple proof of safety, which might be easier (think "TAL").
> Having a proof system integrated into a language does open up interesting new
> degrees of freedom.
Yes. The critical thing that a proof system does is change the boundary
between "safe" and "unsafe". What we traditionally call "safe" languages
are safe in a very conservative sense -- they are *so* safe that the
type system is strong enough to let us *see* that they are safe.
However, there are (at least) two middle positions between
conservatively safe and dynamically unsafe:
dynamically safe (due to run-time checks)
statically safe by virtue of programming idiom, but not in a way that
the compiler can detect.
Dynamically safe programs are not of great interest to the BitC effort,
since they must generate exceptions when the conditions are violated,
and our critical programs must not ever generate exceptions. For other
applications, this might very well be of interest.
Programs that are statically safe by virtue of idiom (we refer to these
as "idiomatically safe") include most major systems applications --
except that the idioms are unchecked and often implemented incorrectly
in places. One of our goals is to try to identify a set of idioms that
(a) are idiomatically safe, but (b) are also things that we can teach
the verifier to check for us.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
