probably the safest (but not necesarilly the easiest) way to go about this is start with an actual type-checking tool, such as the front end to one of the compilers or hatchet http://www.cs.mu.oz.au/~bjpop/hatchet.html and use it to extract every expression of type ∃a . IO a , since your 'verified' program is also typechecked you know no extra IO operations can sneak in anywhere. John On Fri, Oct 04, 2002 at 04:55:06PM +0200, Ch. A. Herrmann wrote:
Hi GHC users,
I'm looking for secure compile and run-time methods to ensure automatically that Haskell modules cannot perform particular IO operations. Therefore, I've got some questions that might be interesting for other people using GHC as well.
o There are functions like "unsafePerformIO". How many of these unsafe functions exist and what are their names? Is there a possibility to tell GHC to reject programs in which such functions occur? Concerning, e.g., the rewrite-rule system, how can we prevent that these functions are applied by some trick, invisible by an automatic inspection of the source code?
o Is the function "print" secure in the sense that all stuff it produces is restricted to go to stdout, even if strange sequences of control characters appear?
o Is there a way to tell the GHC run-time system to block file operations or system calls coming from the application program, while permitting input/output via stdin/stdout?
Thanks in advance -- Christoph Herrmann _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-- --------------------------------------------------------------------------- John Meacham - California Institute of Technology, Alum. - john@foo.net ---------------------------------------------------------------------------