<p>(I'm not in theory; please regard this as a placeholder answer.)</p>

<ol>
<li><p>Is this a research-level question? You may have more luck at <a href="https://cs.stackexchange.com/">cs.stackexchange.com</a>.</p></li>
<li><p>The reason you haven't found much relevant literature may be your choice of keywords. The terms  <em>contract</em> and <em>communication</em> often refer to describing patterns of interaction formed by message passing as a whole, usually abstracting away from the contents of the messages; your contracts, on the other hand, are limitations on the possible contents of individual messages. That subject is better known as <em>validation</em>, and indeed, grammars are routinely used for that purpose.</p></li>
<li><p>Your example uses HTML as the language to restrict, and introduces a BNF for describing it. Don't do that if you can avoid it; SGML and XML were invented for a reason.  They take away the need for you to describe how to recognize syntax trees in strings, so a grammar merely needs to describe a set of allowable trees. XML is a well-established and well-supported standard, and so are several grammar definition formalisms for XML-based languages: XML Schema, Relax-NG, DTDs, Schematron.</p></li>
<li><p>Your example also introduces a technique for describing entity encoding and decoding. SGML and XML come equipped with such a technique, and it is applied in HTML, so why not just use that? (Not that I'm happy with how that works, but it's standard: if you have an XML language, the mechanism is there for you to use.)</p></li>
<li><p>I'm puzzled by <code>@Embeds{URI}</code> - why isn't <code>URI</code> simply a nonterminal?  I can see that its grammar isn't that of HTML, but that of URIs, but XML has a way of dealing with that already: XIncludes and namespaces.  (Not that I'm happy with how that works, but it's standard: if you have an XML language, the mechanism is there for you to use.)</p></li>
<li><p>I don't understand your sanitizers or template context propagators. If you do need a more general annotation mechanism that can be used both to constrain syntax and to interpret it, have a look at stuff such as <a href="http://en.wikipedia.org/wiki/Attribute_grammar" rel="nofollow noreferrer">attribute grammar</a>s, <a href="http://en.wikipedia.org/wiki/Affix_grammar" rel="nofollow noreferrer">affix grammar</a>s and <a href="http://en.wikipedia.org/wiki/Definite_clause_grammar" rel="nofollow noreferrer">definite clause grammar</a>s.  I'm not aware of a pendant for XML, but XSLT can be used in a similar way.</p></li>
<li><p>If the point of sanitizers and template context propagators really is to restrict the HTML language, why not just override the grammar for some nonterminals in the HTML grammar with your own, more restrictive definitions? Both XML Schema and Relax NG support this, although I must add that they don't provide any support for limiting such overrides to defining <em>restrictions</em> only.  An alternative is to use Schematron, in which syntactic constraints are a language construct.</p></li>
<li><p>HTML is an odd choice of language for an example - in a typical web application, there is no great need to constrain the HTML being sent (largely owing to the language being used for markup only and being SGML/XML-based) while it is imperative to put very clear constraints on the messages being accepted in the opposite direction, the HTTP requests. But those are usually simple and don't really use a standard language, unless you put something like SOAP on top. So I'm curious what sort of application you have in mind for this.</p></li>
</ol>

<p>To summarize: yes, there is a lot of support for what you want to do (if I'm not too mistaken about your sanitizers and propagators), especially when the languages you use are XML-based.</p>

CC BY-SA 3.0
2012-05-07T22:53:57.683Z
Taking your points one at a time.  3. SGML and XML don't help with sanitization of HTML -- taking a string of noisy HTML in and producing a string of HTML without powerful instructions that is in the XHTML-like subset that is handled similarly by all major browsers.  There are reasons why the HTML5 specification does not use either to describe HTML -- they can't handle the reality of what browsers do.
Mike Samuel
CC BY-SA 3.0
2012-05-07T22:58:26.057Z
4. I want to make sure encodings faithfully represent the dual of what parsers produce when they decode.  XML languages are just one kind of language that I have to deal with, so are not a substitute for reliable encoder generation.  Encoders are currently hand-written for each library language and are often buggy and inconsistent as a result.  This work is attempting to provide a way to produce encoders of consistent quality for many platforms based on a specification that can be understood by message language experts.
Mike Samuel
CC BY-SA 3.0
2012-05-07T23:01:30.843Z
5. Because all of the URIs in the following are the same `<a href="O'Reilly.html">`, `<a href="O&apos;Reilly.html">`, `<a href="O&APOS;Reilly.html">`, `<a href="O&#39;Reilly.html">`.  I don't want to specify a grammar for a URI and a grammar for a URI embeded in HTML , and a grammar for a URI embedded in CSS, and a grammar for a URI embedded in CSS embedded in HTML (`<a style="background: url('O\27 Reilly&amp; al.css')">`).
Mike Samuel
CC BY-SA 3.0
2012-05-07T23:03:56.097Z
6. There is a [glossary](http://js-quasis-libraries-and-repl.googlecode.com/svn/trunk/safetemplate.html#glossary1) which defines terms like sanitizers and contexts.  In short, templates combine trusted and untrusted data and the context propagation parses small snippets of trusted content so it can figure out the appropriate encoders/sanitizers to use for the untrusted content to preserve the security properties in that same tech report.
Mike Samuel
CC BY-SA 3.0
2012-05-07T23:06:20.680Z
7. Sanitizers and context propagators are not specific to markup languages.  To securely compose HTML, you need to deal with non-markup languages as well - JavaScript, CSS, and URIs are non-markup languages that embed in HTML.
Mike Samuel
CC BY-SA 3.0
2012-05-07T23:08:43.533Z
8. My goal is to make it easy to write distributed (incl. web) applications that do not suffer from injection vulnerabilities.  XSS vulns are 12.8% of all web vulnerabilities according to [Pelizzi et al](http://www.cs.sunysb.edu/~rpelizzi/gdorktr.pdf).  If I can't constrain the HTML being served to prevent code injection, I've failed to address the low hanging fruit.
Mike Samuel
CC BY-SA 3.0
2012-05-16T14:37:32.467Z
Replying one point at a time, too: 3. With validation, it's crucial to know who controls the input you'll be needing to accept. If you can design the constraints yourself, you can do a lot more in validation. If you can't, one approach is to have an explicit preprocessing phase devoted to normalizing the input into some format (e.g. 'sort-of-HTML' might become valid XHTML).  Your last remark leaves me confused: what are you really trying to validate against what?
reinierpost
CC BY-SA 3.0
2012-05-16T14:40:46.423Z
4. What do you mean by 'library language'? Can the role of an encoder/decoder be defined independently of the language?
reinierpost
CC BY-SA 3.0
2012-05-16T14:44:10.070Z
5. I understand, but HTML has its own encoding/escaping mechanism (that isn't specific to URLs), and URLs have their own. Actual web software tends not to conform to either, so if you really want to deal with how real software works, your specification will always follow whatever the software makers happen to implement.
reinierpost
CC BY-SA 3.0
2012-05-16T14:45:16.963Z
8. I don't understand this. Code injection doesn't happen in HTML (i.e. HTTP responses), it happens in HTTP *requests*.
reinierpost
CC BY-SA 3.0
2012-05-16T15:44:41.017Z
In social-media applications, the input comes from multiple sources, some trusted and some not.  I agree re normalizing to XHTML-ish subset.  The formalisms you list are not useful -- HTML5 is not SGML and so there is no DTD that describes it.  Nor is it XML, so XML schemas will not help.
Mike Samuel
CC BY-SA 3.0
2012-05-16T15:53:28.587Z
4. Tools for composing content involve two groups of languages, the language used by the tool user to invoke the tool which is often package as a library/API known as the library language; and the language(s) of the composed content known as the content language.
Mike Samuel
CC BY-SA 3.0
2012-05-16T15:55:34.933Z
5. Agree that HTML and URL have different escaping mechanisms.  I don't see how that is an argument against my explanation of why URI cannot be easily treated as a non-terminal in the HTML grammar.
Mike Samuel
CC BY-SA 3.0
2012-05-16T15:57:27.473Z
8. Not true.  HTTP requests, except maybe for the rare PUT request, do not typically have bodies that are HTML.  Code injection occurs because of errors in the way a web server composes an HTTP response that has content-type:text/html or that the browser guesses is text/html.  XSS is the single most common web vulnerability and is an example of code-injection into HTML that exploits the fact that the same-origin policy applies to all code within an HTML page.
Mike Samuel
CC BY-SA 3.0
2012-05-21T07:43:57.270Z
I think a blog or something like IRC would be a better environment for this discussion.
reinierpost
CC BY-SA 3.0
2012-05-07T21:56:41.423Z
2012-10-18T00:11:56.380Z
2017-04-13T12:48:30.830Z
reinierpost
<p>I am exploring using annotated grammars to formalize and enforce parts of contracts between nodes in a distributed application.</p>

<p>I've found a number of articles on languages for specifying fairly general types of contracts, mostly based around the idea of a contract as a state machine; and others (mostly object-capability schemes) based around the idea of identifying a "safe" subset of a language; but none that use a grammar as the specification of the contract.</p>

<p>I was wondering how attempts to formalize contracts tend to fail, and what else should one keep in mind.</p>

<p>Below are details of the particular kind of contract I am trying to enforce.</p>

<hr>

<p>Given a BNF grammar for part of HTML:</p>

<pre><code>HTML ::== (Text | Link)*;
Text ::== ("&amp;amp;" | "&amp;lt;" | "&amp;quot;" | [^&amp;&lt;"])+;
Link ::== "&lt;a" Href? "&gt;" Text "&lt;/a&gt;";
Href ::== "href=\"" Text+ "\"";
</code></pre>

<p>I can infer which strings are in the language and which are not, and the structure of a parse tree, but by adding annotations thus</p>

<pre><code>HTML ::== (Text | Link)*;
Text ::== @String((@CharValue{"&amp;"}"&amp;amp;"
                 | @CharValue{"&lt;"}"&amp;lt;"
                 | @CharValue{"\""}"&amp;quot;"
                 | [^&amp;&lt;"]))+;
Link ::== "&lt;a" Href? "&gt;" Text? "&lt;/a&gt;";
Href ::== " href=\"" @Embeds{URI}Text+ "\"";
</code></pre>

<p>I can infer additional facts:</p>

<ol>
<li>That plain text can be encoded/decoded by replacing <code>"&amp;"</code> with <code>"&amp;amp;"</code>, etc. and that a string can be encoded as a string that matches the <code>Text</code> non-terminal.</li>
<li>That the URI grammar should be recursively applied to the content of the <code>href</code> post-decoding.</li>
</ol>

<p>From this I hope to generate several artifacts:</p>

<ol>
<li>Encoders.  An encoder for non-terminal T is a <code>'a -&gt; T string</code> function that encodes a data value.</li>
<li>Sanitizers.  A function <code>T string -&gt; T string</code> that produces a similar string that falls in a subset of the language that is well-handled by many different implementations and which does not contain high-power instructions.</li>
<li>A template context propagator.  A function <code>string * context -&gt; string * context</code> which takes a string from a trusted source and the context before the string (context is a type describing a set of prefixes of strings in the language) and produces a string in the well-handled subset of the language and the context after that string is appended to any of the prefixes described by the input context.  This is useful for composing a string from trusted and untrusted code.</li>
</ol>

<p>With these tools, I hope to be able to enforce the contract that any powerful instructions which are parsed by the receiver of a network message composed using these tools are instructions that are present in snippets of code authored by the message sender, and not instructions authored by a provider of untrusted data.</p>

<p>If the sender uses the derived tools to encode or sanitize all untrusted data appropriately, and uses the template propagation algorithm to choose encoders/sanitizers appropriate to the context of the buffer on which the message is being built, then high-power instructions in the buffer must have come from a privileged source.</p>

<p>If the recipient receives a message over a secure channel, and uses the same grammar to parse and decode the message, then it can be confident of the provenance of the instructions it receives.</p>

<p>So the annotated grammar serves as a formal description of a contract, and the tools move the burden of preserving the contract from the application author to the grammar author.  Since there are many application authors who tend to know the well-tested parts of a language, a much smaller number of language specialists who know the poorly tested parts of the grammars as well should be able to make applications robust against code injection.</p>

<fl.formal-languages><cr.crypto-security><grammars><security>
Contract preservation using grammars
Mike Samuel
# Contract preservation using grammars

(Asked by: username_0 on 2012-04-19)

I am exploring using annotated grammars to formalize and enforce parts of contracts between nodes in a distributed application.
I've found a number of articles on languages for specifying fairly general types of contracts, mostly based around the idea of a contract as a state machine; and others (mostly object-capability schemes) based around the idea of identifying a "safe" subset of a language; but none that use a grammar as the specification of the contract.
I was wondering how attempts to formalize contracts tend to fail, and what else should one keep in mind.
Below are details of the particular kind of contract I am trying to enforce.

Given a BNF grammar for part of HTML:
HTML ::== (Text | Link)*;
Text ::== ("&" | "<" | """ | [^&<"])+;
Link ::== "" Text "";
Href ::== "href=\"" Text+ "\"";

I can infer which strings are in the language and which are not, and the structure of a parse tree, but by adding annotations thus
HTML ::== (Text | Link)*;
Text ::== @String((@CharValue{"&"}"&"
                 | @CharValue{"<"}"<"
                 | @CharValue{"\""}"""
                 | [^&<"]))+;
Link ::== "" Text? "";
Href ::== " href=\"" @Embeds{URI}Text+ "\"";

I can infer additional facts:

That plain text can be encoded/decoded by replacing "&" with "&", etc. and that a string can be encoded as a string that matches the Text non-terminal.
That the URI grammar should be recursively applied to the content of the href post-decoding.

From this I hope to generate several artifacts:

Encoders.  An encoder for non-terminal T is a 'a -> T string function that encodes a data value.
Sanitizers.  A function T string -> T string that produces a similar string that falls in a subset of the language that is well-handled by many different implementations and which does not contain high-power instructions.
A template context propagator.  A function string * context -> string * context which takes a string from a trusted source and the context before the string (context is a type describing a set of prefixes of strings in the language) and produces a string in the well-handled subset of the language and the context after that string is appended to any of the prefixes described by the input context.  This is useful for composing a string from trusted and untrusted code.

With these tools, I hope to be able to enforce the contract that any powerful instructions which are parsed by the receiver of a network message composed using these tools are instructions that are present in snippets of code authored by the message sender, and not instructions authored by a provider of untrusted data.
If the sender uses the derived tools to encode or sanitize all untrusted data appropriately, and uses the template propagation algorithm to choose encoders/sanitizers appropriate to the context of the buffer on which the message is being built, then high-power instructions in the buffer must have come from a privileged source.
If the recipient receives a message over a secure channel, and uses the same grammar to parse and decode the message, then it can be confident of the provenance of the instructions it receives.
So the annotated grammar serves as a formal description of a contract, and the tools move the burden of preserving the contract from the application author to the grammar author.  Since there are many application authors who tend to know the well-tested parts of a language, a much smaller number of language specialists who know the poorly tested parts of the grammars as well should be able to make applications robust against code injection.

**Tags:** fl.formal-languages, cr.crypto-security, grammars, security

---

## 1 answers

### Answer by username_1 on 2012-05-07. Score: 1 | Accepted answer

(I'm not in theory; please regard this as a placeholder answer.)

1. Is this a research-level question? You may have more luck at [cs.stackexchange.com](https://cs.stackexchange.com/).
2. The reason you haven't found much relevant literature may be your choice of keywords. The terms *contract* and *communication* often refer to describing patterns of interaction formed by message passing as a whole, usually abstracting away from the contents of the messages; your contracts, on the other hand, are limitations on the possible contents of individual messages. That subject is better known as *validation*, and indeed, grammars are routinely used for that purpose.
3. Your example uses HTML as the language to restrict, and introduces a BNF for describing it. Don't do that if you can avoid it; SGML and XML were invented for a reason. They take away the need for you to describe how to recognize syntax trees in strings, so a grammar merely needs to describe a set of allowable trees. XML is a well-established and well-supported standard, and so are several grammar definition formalisms for XML-based languages: XML Schema, Relax-NG, DTDs, Schematron.
4. Your example also introduces a technique for describing entity encoding and decoding. SGML and XML come equipped with such a technique, and it is applied in HTML, so why not just use that? (Not that I'm happy with how that works, but it's standard: if you have an XML language, the mechanism is there for you to use.)
5. I'm puzzled by `@Embeds{URI}` - why isn't `URI` simply a nonterminal? I can see that its grammar isn't that of HTML, but that of URIs, but XML has a way of dealing with that already: XIncludes and namespaces. (Not that I'm happy with how that works, but it's standard: if you have an XML language, the mechanism is there for you to use.)
6. I don't understand your sanitizers or template context propagators. If you do need a more general annotation mechanism that can be used both to constrain syntax and to interpret it, have a look at stuff such as [attribute grammar](http://en.wikipedia.org/wiki/Attribute_grammar)s, [affix grammar](http://en.wikipedia.org/wiki/Affix_grammar)s and [definite clause grammar](http://en.wikipedia.org/wiki/Definite_clause_grammar)s. I'm not aware of a pendant for XML, but XSLT can be used in a similar way.
7. If the point of sanitizers and template context propagators really is to restrict the HTML language, why not just override the grammar for some nonterminals in the HTML grammar with your own, more restrictive definitions? Both XML Schema and Relax NG support this, although I must add that they don't provide any support for limiting such overrides to defining *restrictions* only. An alternative is to use Schematron, in which syntactic constraints are a language construct.
8. HTML is an odd choice of language for an example - in a typical web application, there is no great need to constrain the HTML being sent (largely owing to the language being used for markup only and being SGML/XML-based) while it is imperative to put very clear constraints on the messages being accepted in the opposite direction, the HTTP requests. But those are usually simple and don't really use a standard language, unless you put something like SOAP on top. So I'm curious what sort of application you have in mind for this.

To summarize: yes, there is a lot of support for what you want to do (if I'm not too mistaken about your sanitizers and propagators), especially when the languages you use are XML-based.

> **Comments:**
> **username_0**: Taking your points one at a time.  3. SGML and XML don't help with sanitization of HTML -- taking a string of noisy HTML in and producing a string of HTML without powerful instructions that is in the XHTML-like subset that is handled similarly by all major browsers.  There are reasons why the HTML5 specification does not use either to describe HTML -- they can't handle the reality of what browsers do.  
> **username_0**: 4. I want to make sure encodings faithfully represent the dual of what parsers produce when they decode.  XML languages are just one kind of language that I have to deal with, so are not a substitute for reliable encoder generation.  Encoders are currently hand-written for each library language and are often buggy and inconsistent as a result.  This work is attempting to provide a way to produce encoders of consistent quality for many platforms based on a specification that can be understood by message language experts.  
> **username_0**: 5. Because all of the URIs in the following are the same `<a href="O'Reilly.html">`, `<a href="O&apos;Reilly.html">`, `<a href="O&APOS;Reilly.html">`, `<a href="O&#39;Reilly.html">`.  I don't want to specify a grammar for a URI and a grammar for a URI embeded in HTML , and a grammar for a URI embedded in CSS, and a grammar for a URI embedded in CSS embedded in HTML (`<a style="background: url('O\27 Reilly&amp; al.css')">`).  
> **username_0**: 6. There is a [glossary](http://js-quasis-libraries-and-repl.googlecode.com/svn/trunk/safetemplate.html#glossary1) which defines terms like sanitizers and contexts.  In short, templates combine trusted and untrusted data and the context propagation parses small snippets of trusted content so it can figure out the appropriate encoders/sanitizers to use for the untrusted content to preserve the security properties in that same tech report.  
> **username_0**: 7. Sanitizers and context propagators are not specific to markup languages.  To securely compose HTML, you need to deal with non-markup languages as well - JavaScript, CSS, and URIs are non-markup languages that embed in HTML.  
> **username_0**: 8. My goal is to make it easy to write distributed (incl. web) applications that do not suffer from injection vulnerabilities.  XSS vulns are 12.8% of all web vulnerabilities according to [Pelizzi et al](http://www.cs.sunysb.edu/~rpelizzi/gdorktr.pdf).  If I can't constrain the HTML being served to prevent code injection, I've failed to address the low hanging fruit.  
> **username_1**: Replying one point at a time, too: 3. With validation, it's crucial to know who controls the input you'll be needing to accept. If you can design the constraints yourself, you can do a lot more in validation. If you can't, one approach is to have an explicit preprocessing phase devoted to normalizing the input into some format (e.g. 'sort-of-HTML' might become valid XHTML).  Your last remark leaves me confused: what are you really trying to validate against what?  
> **username_1**: 4. What do you mean by 'library language'? Can the role of an encoder/decoder be defined independently of the language?  
> **username_1**: 5. I understand, but HTML has its own encoding/escaping mechanism (that isn't specific to URLs), and URLs have their own. Actual web software tends not to conform to either, so if you really want to deal with how real software works, your specification will always follow whatever the software makers happen to implement.  
> **username_1**: 8. I don't understand this. Code injection doesn't happen in HTML (i.e. HTTP responses), it happens in HTTP *requests*.  
> **username_0**: In social-media applications, the input comes from multiple sources, some trusted and some not.  I agree re normalizing to XHTML-ish subset.  The formalisms you list are not useful -- HTML5 is not SGML and so there is no DTD that describes it.  Nor is it XML, so XML schemas will not help.  
> **username_0**: 4. Tools for composing content involve two groups of languages, the language used by the tool user to invoke the tool which is often package as a library/API known as the library language; and the language(s) of the composed content known as the content language.  
> **username_0**: 5. Agree that HTML and URL have different escaping mechanisms.  I don't see how that is an argument against my explanation of why URI cannot be easily treated as a non-terminal in the HTML grammar.  
> **username_0**: 8. Not true.  HTTP requests, except maybe for the rare PUT request, do not typically have bodies that are HTML.  Code injection occurs because of errors in the way a web server composes an HTTP response that has content-type:text/html or that the browser guesses is text/html.  XSS is the single most common web vulnerability and is an example of code-injection into HTML that exploits the fact that the same-origin policy applies to all code within an HTML page.  
> **username_1**: I think a blog or something like IRC would be a better environment for this discussion.  

---

