On Sat, 5 May 2012, "Mark" wrote:
> 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 ..
I didn't know you are still planning to switch back to SML. Anyway, what
did you find nicer about OCaml? As I've said, I was a bit scared by its
proximity to C in many ways, when I did my little YXML implementations in
3 days (half of the time figuring out semantic snags of OCaml string
operations and library modules).
> 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).
The latter is pretty close to what I've meant above. In Poly/ML you can
define how the ML toplevel reads or writes the environment of types,
values, structures etc. so you can do some sandboxing there in a few pages
of ML.
> 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?
I did not look at all details yet. The project looks generally very
interesting, to get a dependable external checker for HOL eventually.
For the moment my main observations are:
* A bit too much extra complication to repair OCaml strings. If you
forget just one immutise in a criticial spot, you have a
vulnerability. Such things need to be right by default, due to the
underlying programming language.
* Still too many obvious attacks are simply declared as forbidden in the
Bounty.txt. Here is the copy from holzero-0.5.4 for the record:
- building HOL Zero from a non-standard ML session state (e.g. with parallelism)
- overwriting key ML objects (e.g. the 'thm' datatype or 'get_all_axioms')
- overwriting the pretty printer for key ML datatypes (e.g. 'thm' or 'list')
- circumventing the ML language proper or its type system (e.g. 'Obj.magic')
- circumventing, reconfiguring or interfering with the ML interpreter
- exploiting bugs in the ML interpreter
- changing the operating system environment in which the ML interpreter runs
I reckon that Milner's LCF had less vulnerabilities.
For example, ML with parallel threads should now be standard, not
non-standard as declared above. It is merely a historical accident that
OCaml is still sequential by default. Your code will require some
additional refinements to make it thread-safe, which requires some "piling
up of more stuff". An alternative would be to nail down the environment
to be always sequential.
Makarius
------------------------------------------------------------------------------
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
