'safe' prolog meta-circular interpreter

[Chris Mungall]

Let's say I wanted to allow people to send queries to a prolog  
database over http. This would obviously be a massive security hole.

However, if their query/program was limited to a fixed set of  
predicates (no I/O), and there was a clever way to check the second  
argument of bagof/3 then could this be made safe?

The safest way would be through a meta-circular interpreter; a more  
efficient but perhaps more difficult way would be through static  
analysis (HiLog would be banned, making this easier)

Are there any implementations out there?

Cheers
Chris

------------
For further info, please visit http://www.swi-prolog.org/

To unsubscribe, send a plaintext mail with "unsubscribe prolog <e-mail>"
in its body to majordomo@...

[Richard A. O'Keefe]

On 16 Jan 2007, at 5:46 am, Chris Mungall wrote:

> Let's say I wanted to allow people to send queries to a prolog  
> database over http. This would obviously be a massive security hole.

Right.
>
>
> However, if their query/program was limited to a fixed set of  
> predicates (no I/O), and there was a clever way to check the second  
> argument of bagof/3 then could this be made safe?

Sure.  Trivial proof: limit the set of predicates to true/0 and fail/0.
>

> The safest way would be through a meta-circular interpreter; a more  
> efficient but perhaps more difficult way would be through static  
> analysis (HiLog would be banned, making this easier)

What do you need a meta-circular interpreter for?
(For one thing, why should your query language be able to interpret  
itself?)
You need to define SOME query language using Prolog term syntax
(given that you want to send Prolog terms over the link).
You need to have SOME safety filter which walks over a query
in your query language, "compiling" it to a Prolog goal as you
go.  In easy cases, compiling could be the identity transformation.
You then execute the query using call/1.

_In general_ using call/1 is a security hole,
but not when you have just checked that it's OK.
>

> Are there any implementations out there?

The process as described is pretty trivial.
A starting point might be
        "A query is OK if it is
         - a callable term which is
         - a call to a predicate exported from 'mysafe:' module or
         - a call to one of a short list of built in predicates or
         - a bunch of safe queries combined using _, _
           _ ; _    _ -> _    _ -> _ ; _    \+ (_)
           or any other control structures you deem safe."
Compilation adds 'mysafe:' in front of the subgoals that need it.
Labour: about one page of trivial code.


------------
For further info, please visit http://www.swi-prolog.org/

To unsubscribe, send a plaintext mail with "unsubscribe prolog <e-mail>"
in its body to majordomo@...

[Jan Wielemaker]

On Wednesday 30 April 2008 12:36:21 Richard A. O'Keefe wrote:

> On 16 Jan 2007, at 5:46 am, Chris Mungall wrote:
> > Let's say I wanted to allow people to send queries to a prolog
> > database over http. This would obviously be a massive security hole.
>
> Right.
>
> > However, if their query/program was limited to a fixed set of
> > predicates (no I/O), and there was a clever way to check the second
> > argument of bagof/3 then could this be made safe?
>
> Sure.  Trivial proof: limit the set of predicates to true/0 and fail/0.
>
> > The safest way would be through a meta-circular interpreter; a more
> > efficient but perhaps more difficult way would be through static
> > analysis (HiLog would be banned, making this easier)
>
> What do you need a meta-circular interpreter for?
> (For one thing, why should your query language be able to interpret
> itself?)
> You need to define SOME query language using Prolog term syntax
> (given that you want to send Prolog terms over the link).
> You need to have SOME safety filter which walks over a query
> in your query language, "compiling" it to a Prolog goal as you
> go.  In easy cases, compiling could be the identity transformation.
> You then execute the query using call/1.
>
> _In general_ using call/1 is a security hole,
> but not when you have just checked that it's OK.
>
> > Are there any implementations out there?
>
> The process as described is pretty trivial.
> A starting point might be
> "A query is OK if it is
> - a callable term which is
> - a call to a predicate exported from 'mysafe:' module or
> - a call to one of a short list of built in predicates or
> - a bunch of safe queries combined using _, _
>   _ ; _    _ -> _    _ -> _ ; _    \+ (_)
>   or any other control structures you deem safe."
> Compilation adds 'mysafe:' in front of the subgoals that need it.
> Labour: about one page of trivial code.

There is actually some additional trickery. SWI-Prolog modules have a
notion of a `default module'. If it cannot find a predicate it looks at
the default module and imports the predicate. All modules default to
'user', which defaults to 'system', where all system predicates are
defined. You can change this using import_module/2 and
delete_import_module/2.  So, by doing

?- delete_import_module(mysafe, user).

the module mysafe no longer imports _new_ system predicates. Also
disable library autoloading for the module. Now make a bunch of calls to
import/1 to get the predicates you consider safe to module mysafe. This
would be a nice and perfect jail if you couldn't call Module:Goal.

If we could add something to prevent this escape it is easy to create a
library with different levels of security. To make a playground, just
create a new module, delete the user normal import module, stop autoload
and add the appropriate secure module as import module.

To execute code safely, load it into this module and call it.

        --- Jan


------------
For further info, please visit http://www.swi-prolog.org/

To unsubscribe, send a plaintext mail with "unsubscribe prolog <e-mail>"
in its body to majordomo@...