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
o There are functions like "unsafePerformIO". How many of these unsafe functions exist and what are their names? Is there
It depends on what you count as unsafe. There's also unsafeIOToST, which is just as unsafe (You can write unsafePerformIO using this -- see a message to the haskell list from Koen Classen from a while back). There are also functions like unsafeRead on arrays, which is unsafe in the sense that it doesn't do bounds checking.
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?
Not if the posix library is used. If that is used, you can use dupto to redirect output from stdout to any file.
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?
I can't say for sure, but I would guess not. Based on recent discussion about exactly how to handle stdin/stdout, it seems to be beyond the scope of a language to prescribe these things...
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 ---------------------------------------------------------------------------
participants (3)
-
Ch. A. Herrmann -
Hal Daume III -
John Meacham