Contract preservation using grammars

Question

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 ::== ("&amp;" | "&lt;" | "&quot;" | [^&<"])+;
Link ::== "<a" Href? ">" Text "</a>";
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{"<"}"&lt;"
                 | @CharValue{"\""}"&quot;"
                 | [^&<"]))+;
Link ::== "<a" Href? ">" Text? "</a>";
Href ::== " href=\"" @Embeds{URI}Text+ "\"";

I can infer additional facts:

1. 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.
2. That the URI grammar should be recursively applied to the content of the href post-decoding.

From this I hope to generate several artifacts:

1. Encoders. An encoder for non-terminal T is a 'a -> T string function that encodes a data value.
2. 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.
3. 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.

Answer 1

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

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 grammars, affix grammars and definite clause grammars. 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.