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 > [EMAIL PROTECTED] > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > -- --------------------------------------------------------------------------- John Meacham - California Institute of Technology, Alum. - [EMAIL PROTECTED] --------------------------------------------------------------------------- _______________________________________________ Glasgow-haskell-users mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
