Sorry for being a little late to join the discussion. At the risk of going down a side alley, I feel I need to respond to some points related to trustworthiness and/or HOL Zero.
Makarius wrote: > A system like HOL-Light has the advantage that the reader gets > quickly an impression what the basic logic functionality is > meant to be. This gives some certainty under additional > assumptions, i.e. that the ML really is what it seems at first > sight, and that certain bad things are not done in practice. Yes, and, inspired by HOL Light, I took this further with HOL Zero, by trying to make the source code even easier to follow, and by giving extensive source code comments explaining exactly what is going on. Freek wrote: > Surely in every practical programming language you can > "cheat" in some way if you try hard enough. For instance by > poking the memory, either internally through some Obj.magic > like interface, or if you don't get that from your language > by poking in /dev/mem? Yes, but if we can push these vulnerabilities into as small as possible corner of the programming language toplevel (e.g. OCaml's Obj.magic and the C and OS interfaces), then this gives us something useful. We can have a well-defined subset of dodgy stuff, where everything else is safe. For those of us that have concern about soundness (e.g. anyone trying to audit a massive industrial safety-critical formal verification project), this is a considerably better situation than simply throwing our hands up in the air and saying "well, we can never be certain about anything" (apologies for over-simplifying your stance, Freek). So this is what I've been trying to do with HOL Zero - to define as clearly as possible what is and what isn't safe, and to maximise this safe subset of behaviour. This definition is not perfect yet, but the safe subset is considerably larger and considerably better defined than in any other proof system I know of. And if anyone finds a problem and tells me about it, I award them with $100 and the problem gets published on my website (even the ones I find, although I don't bother giving myself $100). Makarius wrote: > Mark Adams occasionally promotes an even more aggressive > scenario for HOL Zero where he wants to admit potentially > malicious users, an army of paid proof-workers who want to > cheat. (I am not really following him here, we are not that > far yet.) Yes, I do. I think we are already close to this. Freek wrote: > So the possibility of cheating if you really try does not > seem an interesting one to me. What's important is that > you won't "cheat" accidentally, by misunderstanding how > things work. In my experience, in some large industrial formal verifications, where you are writing 15,000 lines of bespoke ML extension to a theorem prover, to automate the proof of 1,000-line automatically-generated conjectures, it is virtually impossible to define what is and what isn't feasibly accidental. I certainly came across situations that I had subconsciously dismissed as impossible, or that I thought would never occur in practice. I think we should be striving to make it as difficult as possible to cheat, whether maliciously or accidentally. Makarius wrote: > This Obj stuff is absent in SML. Yes and I plan to port HOL Zero to SML. SML is fundamentally safer and better defined than OCaml. I think I would have used SML from the onset if I knew about these OCaml vulnerabilities. Although OCaml is nicer in other ways .. Makarius wrote: > Moreover, as I have explained to Mark Adams already in a > similar discussion, one can seal up the toplevel > interpreter loop, to isolate user scripts from any such > built-in nonsense. ... A managed ML toplevel is again > one of these layers that would complicate a prover > implementation, but make it more reliable. .... These techniques have the effect of removing vulnerabilities, but at the expense of greatly complicating the implementation, perhaps introducing their own vulnerabilities. What I would really like is an ML interpreter with a toplevel that can be configured to disallow all nasty stuff (e.g. overwriting the 'thm' datatype, or overwriting its pretty printer). Makarius wrote: > I've looked at holzero-0.4.1 before and just today at > holzero-0.5.4. (I am still hoping to see a really > convincing independent proof checker for the HOL family > of systems.) In what sense is HOL Zero not a convincincly independent implementation of the HOL logic? Its development was sponsored by no-one other than myself. Its core system (inference kernel + parser/printer + core theory) was all genuinely written from scratch - it took about 5 iterations to get variable instantiation right!! Its architecture involves the innovation of an inner (or "language") kernel, inside the inference kernel. Its parser, printer and concrete syntax involve numerous innovations; they are, for the first time in a HOL system, compatible, well-behaved and input-complete (according to definitions in Freek's Pollack Inconsistency paper). The specification (but not implementation) of its 800 ML interface objects (equivalents of 'assoc', 'frees', 'INST', etc) was largely derived from the pre-existing HOL systems, but this was done by careful consideration of each system's behaviour in turn. Makarius wrote: > My impression is now that he *is* piling up more and > more stuff to make up for the semantic weaknesses > of OCaml for his project. The only example I can think of is my solution for the problem of OCaml's mutable strings, which just adds a single line of code to a few vital kernel functions. Is there anything else? Makarius wrote: > Sealing up such holes makes the implementation more > complex. For example, the Coq people have their own > version of int and string that really mean int and > string in a mathematical sense, without silent > overflow or hidden mutation. > > Driving this further and further, adding infrastructure > to address weaknesses of the implementation and other > side-conditions, you get to a highly complex system > like Isabelle. I really think that with just a little support from an ML interpreter that can be configured to ban nasty stuff, then a simple theorem prover can seal up the holes and yet be extremely simple. We don't need to define our own ints or strings or sandboxes. Milner's approach achieves it with a simple system, if implemented carefully enough. For those interested in HOL Zero, its implementation is about complete, but the user manual is not. The next release of HOL Zero, out in a month or two, will have a complete user manual. 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
