(Apologies if this arrives as a multiple post. It was first posted to
comp.lang.lisp and
comp.lang.functional four hours ago.)
People have written in to me asking 'Can you define polyadic functions
in Qi and use them in a type secure way?' The answer is 'yes you
can'.
This example uses a really simple type secure HTML formatter for you
to extend. It is based on a 1-line polyadic function defined in CL.
(DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
Tag))
Thus
(html html
(html head
(html title "Test"))
(html body
(html p "Just some text")))
generates basic HTML
"<html> <head> <title> Test </title> </head> <body> <p> Just some
text </p>
</body> </html>"
The type theory is more complex. html is a polyadic function that can
assume n arguments where n > 1. In such a case we need to define a
special type theory for html. Here it is
(datatype html
Tag : symbol; String : string;
_______________________________
(html Tag String) : string;
if (cons? HTML)
if (= (head HTML) html)
if (> (length HTML) 3)
let String (nth 3 HTML)
let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
HTML)))]
String : string; NewHTML : string;
_________________________________
HTML : string;)
The first (base) case is where n = 2 - it says that html accepts a
symbol and a string and outputs a string.
The second case deals with n > 2 - it says that html returns a string
just when the
second argument is a string and the expression that results from
removing this
argument also returns a string. This recursively shortens the
expression towards the
base case.
Since html is a polyadic function and has no type of and by itself, we
do not support
currying for it. This means in Qi-speak it is a *special form* - one
that does not support currying. We need to tell Qi not to try to
curry this form of expression and to treat it as special. This does
the trick.
(specialise html)
So if I put all this in a file "html.txt"
(DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
Tag))
(specialise html)
(datatype html
Tag : symbol; String : string;
_______________________________
(html Tag String) : string;
if (cons? HTML)
if (= (head HTML) html)
if (> (length HTML) 3)
let String (nth 3 HTML)
let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
HTML)))]
String : string; NewHTML : string;
_________________________________
HTML : string;)
I can enter (load "html.txt") in Qi and load the lot.* I can now use
it in a type
secure Qi environment.
(24+) (html html
(html head
(html title "Test"))
(html body
(html p "Just some text")))
"<html> <head> <title> Test </title> </head> <body> <p> Just some
text </p>
</body> </html>" : string
Once you've got this far you can do other things - like creating your
own type secure
formatting shorthand in the style of CL-WHO
(define :head
{string --> string}
Text -> (html head Text))
(define :title
{string --> string}
Title -> (html title Title))
(define :p
{string --> string}
Para -> (html p Para))
So
(html html
(html head
(html title "Test"))
(html body
(html p "Just some text")))
becomes
(html html
(:head
(:title "Test"))
(html body
(:p "Just some text")))
"<html> <head> <title> Test </title> </head> <body> <p> Just some
text </p>
</body> </html>" : string
If you want to go further and really make it tight you can replace
Tag : symbol; ....
in my datatype by
Tag : tag; ....
and define the type tag to ensure that users cannot generate garbage
HTML with
nonsense tags. But you've probably got the idea by now and I'll leave
the rest to you.
This post is study #8 in 'Studies in Qi'
(http://www.lambdassociates.org/studies/study08.htm)
Mark
* Note generally its smart to put Qi and Lisp in seperate files and
use the Qi 'load'
to load Qi and the CL 'LOAD' to load the CL because the readers are
slightly different.
Here we can get away with mixing. It is important to declare html
to be a special form
before we declare the datatype otherwise Qi will use currying in the
datatype definition.
On Jun 28, 6:09 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> (Apologies if this arrives as a multiple post. It was first posted to
> comp.lang.lisp and
> comp.lang.functional four hours ago.)
>
> People have written in to me asking 'Can you define polyadic functions
> in Qi and use them in a type secure way?' The answer is 'yes you
> can'.
>
> This example uses a really simple type secure HTML formatter for you
> to extend. It is based on a 1-line polyadic function defined in CL.
>
> (DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
> Tag))
>
> Thus
>
> (html html
> (html head
> (html title "Test"))
> (html body
> (html p "Just some text")))
>
> generates basic HTML
>
> "<html> <head> <title> Test </title> </head> <body> <p> Just some
> text </p>
> </body> </html>"
>
> The type theory is more complex. html is a polyadic function that can
> assume n arguments where n > 1. In such a case we need to define a
> special type theory for html. Here it is
>
> (datatype html
>
> Tag : symbol; String : string;
> _______________________________
> (html Tag String) : string;
>
> if (cons? HTML)
> if (= (head HTML) html)
> if (> (length HTML) 3)
> let String (nth 3 HTML)
> let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
> HTML)))]
> String : string; NewHTML : string;
> _________________________________
> HTML : string;)
>
> The first (base) case is where n = 2 - it says that html accepts a
> symbol and a string and outputs a string.
>
> The second case deals with n > 2 - it says that html returns a string
> just when the
> second argument is a string and the expression that results from
> removing this
> argument also returns a string. This recursively shortens the
> expression towards the
> base case.
>
> Since html is a polyadic function and has no type of and by itself, we
> do not support
> currying for it. This means in Qi-speak it is a *special form* - one
> that does not support currying. We need to tell Qi not to try to
> curry this form of expression and to treat it as special. This does
> the trick.
>
> (specialise html)
>
> So if I put all this in a file "html.txt"
>
> (DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
> Tag))
>
> (specialise html)
>
> (datatype html
>
> Tag : symbol; String : string;
> _______________________________
> (html Tag String) : string;
>
> if (cons? HTML)
> if (= (head HTML) html)
> if (> (length HTML) 3)
> let String (nth 3 HTML)
> let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
> HTML)))]
> String : string; NewHTML : string;
> _________________________________
> HTML : string;)
>
> I can enter (load "html.txt") in Qi and load the lot.* I can now use
> it in a type
> secure Qi environment.
>
> (24+) (html html
> (html head
> (html title "Test"))
> (html body
> (html p "Just some text")))
> "<html> <head> <title> Test </title> </head> <body> <p> Just some
> text </p>
> </body> </html>" : string
>
> Once you've got this far you can do other things - like creating your
> own type secure
> formatting shorthand in the style of CL-WHO
>
> (define :head
> {string --> string}
> Text -> (html head Text))
>
> (define :title
> {string --> string}
> Title -> (html title Title))
>
> (define :p
> {string --> string}
> Para -> (html p Para))
>
> So
>
> (html html
> (html head
> (html title "Test"))
> (html body
> (html p "Just some text")))
>
> becomes
>
> (html html
> (:head
> (:title "Test"))
> (html body
> (:p "Just some text")))
> "<html> <head> <title> Test </title> </head> <body> <p> Just some
> text </p>
> </body> </html>" : string
>
> If you want to go further and really make it tight you can replace
>
> Tag : symbol; ....
>
> in my datatype by
>
> Tag : tag; ....
>
> and define the type tag to ensure that users cannot generate garbage
> HTML with
> nonsense tags. But you've probably got the idea by now and I'll leave
> the rest to you.
>
> This post is study #8 in 'Studies in Qi'
>
> (http://www.lambdassociates.org/studies/study08.htm)
>
> Mark
>
> * Note generally its smart to put Qi and Lisp in seperate files and
> use the Qi 'load'
> to load Qi and the CL 'LOAD' to load the CL because the readers are
> slightly different.
> Here we can get away with mixing. It is important to declare html
> to be a special form
> before we declare the datatype otherwise Qi will use currying in the
> datatype definition.
Mark is it possible to use Qi type as a protection from cross site
scripting & SQL injections, something like creating a Qi type that
will handle user entered text at my web application?
Slobodan Blazeski
On 29 Jun, 12:23, Slobodan Blazeski <·················@gmail.com>
wrote:
> On Jun 28, 6:09 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
>
>
>
>
>
> > (Apologies if this arrives as a multiple post. It was first posted to
> > comp.lang.lisp and
> > comp.lang.functional four hours ago.)
>
> > People have written in to me asking 'Can you define polyadic functions
> > in Qi and use them in a type secure way?' The answer is 'yes you
> > can'.
>
> > This example uses a really simple type secure HTML formatter for you
> > to extend. It is based on a 1-line polyadic function defined in CL.
>
> > (DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
> > Tag))
>
> > Thus
>
> > (html html
> > (html head
> > (html title "Test"))
> > (html body
> > (html p "Just some text")))
>
> > generates basic HTML
>
> > "<html> <head> <title> Test </title> </head> <body> <p> Just some
> > text </p>
> > </body> </html>"
>
> > The type theory is more complex. html is a polyadic function that can
> > assume n arguments where n > 1. In such a case we need to define a
> > special type theory for html. Here it is
>
> > (datatype html
>
> > Tag : symbol; String : string;
> > _______________________________
> > (html Tag String) : string;
>
> > if (cons? HTML)
> > if (= (head HTML) html)
> > if (> (length HTML) 3)
> > let String (nth 3 HTML)
> > let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
> > HTML)))]
> > String : string; NewHTML : string;
> > _________________________________
> > HTML : string;)
>
> > The first (base) case is where n = 2 - it says that html accepts a
> > symbol and a string and outputs a string.
>
> > The second case deals with n > 2 - it says that html returns a string
> > just when the
> > second argument is a string and the expression that results from
> > removing this
> > argument also returns a string. This recursively shortens the
> > expression towards the
> > base case.
>
> > Since html is a polyadic function and has no type of and by itself, we
> > do not support
> > currying for it. This means in Qi-speak it is a *special form* - one
> > that does not support currying. We need to tell Qi not to try to
> > curry this form of expression and to treat it as special. This does
> > the trick.
>
> > (specialise html)
>
> > So if I put all this in a file "html.txt"
>
> > (DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
> > Tag))
>
> > (specialise html)
>
> > (datatype html
>
> > Tag : symbol; String : string;
> > _______________________________
> > (html Tag String) : string;
>
> > if (cons? HTML)
> > if (= (head HTML) html)
> > if (> (length HTML) 3)
> > let String (nth 3 HTML)
> > let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
> > HTML)))]
> > String : string; NewHTML : string;
> > _________________________________
> > HTML : string;)
>
> > I can enter (load "html.txt") in Qi and load the lot.* I can now use
> > it in a type
> > secure Qi environment.
>
> > (24+) (html html
> > (html head
> > (html title "Test"))
> > (html body
> > (html p "Just some text")))
> > "<html> <head> <title> Test </title> </head> <body> <p> Just some
> > text </p>
> > </body> </html>" : string
>
> > Once you've got this far you can do other things - like creating your
> > own type secure
> > formatting shorthand in the style of CL-WHO
>
> > (define :head
> > {string --> string}
> > Text -> (html head Text))
>
> > (define :title
> > {string --> string}
> > Title -> (html title Title))
>
> > (define :p
> > {string --> string}
> > Para -> (html p Para))
>
> > So
>
> > (html html
> > (html head
> > (html title "Test"))
> > (html body
> > (html p "Just some text")))
>
> > becomes
>
> > (html html
> > (:head
> > (:title "Test"))
> > (html body
> > (:p "Just some text")))
> > "<html> <head> <title> Test </title> </head> <body> <p> Just some
> > text </p>
> > </body> </html>" : string
>
> > If you want to go further and really make it tight you can replace
>
> > Tag : symbol; ....
>
> > in my datatype by
>
> > Tag : tag; ....
>
> > and define the type tag to ensure that users cannot generate garbage
> > HTML with
> > nonsense tags. But you've probably got the idea by now and I'll leave
> > the rest to you.
>
> > This post is study #8 in 'Studies in Qi'
>
> > (http://www.lambdassociates.org/studies/study08.htm)
>
> > Mark
>
> > * Note generally its smart to put Qi and Lisp in seperate files and
> > use the Qi 'load'
> > to load Qi and the CL 'LOAD' to load the CL because the readers are
> > slightly different.
> > Here we can get away with mixing. It is important to declare html
> > to be a special form
> > before we declare the datatype otherwise Qi will use currying in the
> > datatype definition.
>
> Mark is it possible to use Qi type as a protection from cross site
> scripting & SQL injections, something like creating a Qi type that
> will handle user entered text at my web application?
>
> Slobodan Blazeski- Hide quoted text -
>
> - Show quoted text -
I'm not a web guru; *I'd suggest posting this query to Qilang.*
There's > 50 members some of whom will have more extensive web
experience than me. What I have to say should be filled out by
seasoned web gurus and taken cum grano salis because I claim no
authority here.
Cross site scripting was unknown to me before you raised it.
_________________________________________________________
>From http://www.cgisecurity.com/articles/xss-faq.shtml#whatis
Cross site scripting (also known as XSS) occurs when a web application
gathers malicious data from a user. The data is usually gathered in
the form of a hyperlink which contains malicious content within it.
The user will most likely click on this link from another website,
instant message, or simply just reading a web board or email message.
>From http://en.wikipedia.org/wiki/Cross-site_scripting
Cross-site scripting (XSS) is a type of computer security
vulnerability typically found in web applications which allow code
injection by malicious web users into the web pages viewed by other
users.
__________________________________________________________________
I understand from this that XSS occurs as a result of uploading
malicious material in an interactive web site (e.g. a notice board).
This material then targets the user or possibly the server on which
the site is built. Is that right?
OK; if thats right then the problem reduces to the detection of
malicious or potentially dangerous material in a pile of free text.
This *can* be phrased as a type checking problem although it may just
as easily phrased as a parsing problem or a pattern/string searching
problem. Type checking is rather more powerful than that, but the
extra power may or may not be useful in this context e.g. spam
detection or XXX material detection is not really a type problem.
Where type checking is definitely useful is in restricting and
defining acceptable
language constructions in a formal language context. You can use Qi
type checking to implement executable type theories for languages that
otherwise lack them - including artificial sub-languages that
correspond to no well-known paradigm. Have a look at study #2 in
www.lambdassociates.org/studies/study02.htm which defines a type
theory for a language very like CL.
So .... if you are working with/uploading a scripting language or any
web-based language which includes insecure features that you feel
might jeopardise your or your users' safety critical applications, you
can fairly easily define a type theory in Qi for a subset of that
language which excludes the dangerous features you want to block. In
my example above, by defining 'tag' you can define a formatting
language that selects almost any proper subset of HTML.
This is one powerful application of Qi - to the validation of bespoke
languages that are tailored subsets of recognised languages - tailored
for security aspects specific to the application at hand.
Mark
On Jun 29, 7:32 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> On 29 Jun, 12:23, Slobodan Blazeski <·················@gmail.com>
> wrote:
>
>
>
> > On Jun 28, 6:09 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
>
> > > (Apologies if this arrives as a multiple post. It was first posted to
> > > comp.lang.lisp and
> > > comp.lang.functional four hours ago.)
>
> > > People have written in to me asking 'Can you define polyadic functions
> > > in Qi and use them in a type secure way?' The answer is 'yes you
> > > can'.
>
> > > This example uses a really simple type secure HTML formatter for you
> > > to extend. It is based on a 1-line polyadic function defined in CL.
>
> > > (DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
> > > Tag))
>
> > > Thus
>
> > > (html html
> > > (html head
> > > (html title "Test"))
> > > (html body
> > > (html p "Just some text")))
>
> > > generates basic HTML
>
> > > "<html> <head> <title> Test </title> </head> <body> <p> Just some
> > > text </p>
> > > </body> </html>"
>
> > > The type theory is more complex. html is a polyadic function that can
> > > assume n arguments where n > 1. In such a case we need to define a
> > > special type theory for html. Here it is
>
> > > (datatype html
>
> > > Tag : symbol; String : string;
> > > _______________________________
> > > (html Tag String) : string;
>
> > > if (cons? HTML)
> > > if (= (head HTML) html)
> > > if (> (length HTML) 3)
> > > let String (nth 3 HTML)
> > > let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
> > > HTML)))]
> > > String : string; NewHTML : string;
> > > _________________________________
> > > HTML : string;)
>
> > > The first (base) case is where n = 2 - it says that html accepts a
> > > symbol and a string and outputs a string.
>
> > > The second case deals with n > 2 - it says that html returns a string
> > > just when the
> > > second argument is a string and the expression that results from
> > > removing this
> > > argument also returns a string. This recursively shortens the
> > > expression towards the
> > > base case.
>
> > > Since html is a polyadic function and has no type of and by itself, we
> > > do not support
> > > currying for it. This means in Qi-speak it is a *special form* - one
> > > that does not support currying. We need to tell Qi not to try to
> > > curry this form of expression and to treat it as special. This does
> > > the trick.
>
> > > (specialise html)
>
> > > So if I put all this in a file "html.txt"
>
> > > (DEFUN html (Tag &REST Text) (FORMAT NIL "<~A> ~{ ~A~} </~A>" Tag Text
> > > Tag))
>
> > > (specialise html)
>
> > > (datatype html
>
> > > Tag : symbol; String : string;
> > > _______________________________
> > > (html Tag String) : string;
>
> > > if (cons? HTML)
> > > if (= (head HTML) html)
> > > if (> (length HTML) 3)
> > > let String (nth 3 HTML)
> > > let NewHTML [(nth 1 HTML) (nth 2 HTML) | (tail (tail (tail
> > > HTML)))]
> > > String : string; NewHTML : string;
> > > _________________________________
> > > HTML : string;)
>
> > > I can enter (load "html.txt") in Qi and load the lot.* I can now use
> > > it in a type
> > > secure Qi environment.
>
> > > (24+) (html html
> > > (html head
> > > (html title "Test"))
> > > (html body
> > > (html p "Just some text")))
> > > "<html> <head> <title> Test </title> </head> <body> <p> Just some
> > > text </p>
> > > </body> </html>" : string
>
> > > Once you've got this far you can do other things - like creating your
> > > own type secure
> > > formatting shorthand in the style of CL-WHO
>
> > > (define :head
> > > {string --> string}
> > > Text -> (html head Text))
>
> > > (define :title
> > > {string --> string}
> > > Title -> (html title Title))
>
> > > (define :p
> > > {string --> string}
> > > Para -> (html p Para))
>
> > > So
>
> > > (html html
> > > (html head
> > > (html title "Test"))
> > > (html body
> > > (html p "Just some text")))
>
> > > becomes
>
> > > (html html
> > > (:head
> > > (:title "Test"))
> > > (html body
> > > (:p "Just some text")))
> > > "<html> <head> <title> Test </title> </head> <body> <p> Just some
> > > text </p>
> > > </body> </html>" : string
>
> > > If you want to go further and really make it tight you can replace
>
> > > Tag : symbol; ....
>
> > > in my datatype by
>
> > > Tag : tag; ....
>
> > > and define the type tag to ensure that users cannot generate garbage
> > > HTML with
> > > nonsense tags. But you've probably got the idea by now and I'll leave
> > > the rest to you.
>
> > > This post is study #8 in 'Studies in Qi'
>
> > > (http://www.lambdassociates.org/studies/study08.htm)
>
> > > Mark
>
> > > * Note generally its smart to put Qi and Lisp in seperate files and
> > > use the Qi 'load'
> > > to load Qi and the CL 'LOAD' to load the CL because the readers are
> > > slightly different.
> > > Here we can get away with mixing. It is important to declare html
> > > to be a special form
> > > before we declare the datatype otherwise Qi will use currying in the
> > > datatype definition.
>
> > Mark is it possible to use Qi type as a protection from cross site
> > scripting & SQL injections, something like creating a Qi type that
> > will handle user entered text at my web application?
>
> > Slobodan Blazeski- Hide quoted text -
>
> > - Show quoted text -
>
> I'm not a web guru; *I'd suggest posting this query to Qilang.*
> There's > 50 members some of whom will have more extensive web
> experience than me. What I have to say should be filled out by
> seasoned web gurus and taken cum grano salis because I claim no
> authority here.
>
> Cross site scripting was unknown to me before you raised it.
>
> _________________________________________________________
>
> >Fromhttp://www.cgisecurity.com/articles/xss-faq.shtml#whatis
>
> Cross site scripting (also known as XSS) occurs when a web application
> gathers malicious data from a user. The data is usually gathered in
> the form of a hyperlink which contains malicious content within it.
> The user will most likely click on this link from another website,
> instant message, or simply just reading a web board or email message.
>
> >Fromhttp://en.wikipedia.org/wiki/Cross-site_scripting
>
> Cross-site scripting (XSS) is a type of computer security
> vulnerability typically found in web applications which allow code
> injection by malicious web users into the web pages viewed by other
> users.
> __________________________________________________________________
>
> I understand from this that XSS occurs as a result of uploading
> malicious material in an interactive web site (e.g. a notice board).
> This material then targets the user or possibly the server on which
> the site is built. Is that right?
>
> OK; if thats right then the problem reduces to the detection of
> malicious or potentially dangerous material in a pile of free text.
> This *can* be phrased as a type checking problem although it may just
> as easily phrased as a parsing problem or a pattern/string searching
> problem. Type checking is rather more powerful than that, but the
> extra power may or may not be useful in this context e.g. spam
> detection or XXX material detection is not really a type problem.
>
> Where type checking is definitely useful is in restricting and
> defining acceptable
> language constructions in a formal language context. You can use Qi
> type checking to implement executable type theories for languages that
> otherwise lack them - including artificial sub-languages that
> correspond to no well-known paradigm. Have a look at study #2 inwww.lambdassociates.org/studies/study02.htmwhich defines a type
> theory for a language very like CL.
>
> So .... if you are working with/uploading a scripting language or any
> web-based language which includes insecure features that you feel
> might jeopardise your or your users' safety critical applications, you
> can fairly easily define a type theory in Qi for a subset of that
> language which excludes the dangerous features you want to block.
it's better to use allow than deny because it's hard to deny all
potential abuse possibilities.
> In
> my example above, by defining 'tag' you can define a formatting
> language that selects almost any proper subset of HTML.
>
> This is one powerful application of Qi - to the validation of bespoke
> languages that are tailored subsets of recognised languages - tailored
> for security aspects specific to the application at hand.
>
> Mark
Thanks Mark ,I already read the study . Maybe Qi is overkill but
definately worth a shot.
Slobodan Blazeski