IO security

[John Meacham]

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
---------------------------------------------------------------------------