On Sun, 2007-01-28 at 11:08 -0800, Mark S. Miller wrote: > Jonathan S. Shapiro wrote: > > The "free" keyword is reserved, but allowing it to be invoked without > > discharge creates safety issues. Having said that, I should admit a > > sleazy hidden fact: the prover will need DEFAXIOM to allow programmers > > to introduce facts that cannot be proved. In particular, DEFAXIOM is > > needed to describe the behavior of assembly support routines. So free > > can be used badly if desired. > > Could the use of unsafe-free be controlled, in much the way that BitC > currently controls the ability to introduce mutable static state? If not, > then > a malicious library writer can use unsafe-free to violate memory safety.
The control is the proof. Unfortunately, some facts have to come from outside the proof. Mark: you are seeking a degree of trust that BitC cannot deliver and still meet its design objectives. The best answer to what you ask is "disallow explicit free". Yes, we can and will provide a means to check for that at link time. > Any module that has permission to unsafe-free is a central point of failure > for that process as a whole, since the correct function of everything else in > that process relies on that module to use unsafe-free safely. > > [1] http://www.hpl.hp.com/techreports/2006/HPL-2006-116.html No. Any module that has permission to unsafe-free without a corresponding proof discharge is such a central point of failure. shap -- Jonathan S. Shapiro, Ph.D. Managing Director The EROS Group, LLC +1 443 927 1719 x5100 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
