By Dakota Williams –
Languages are tools to describe different types of problems. The problem this semester was access control and authentication. In the book, Access Control, Security, and Trust: A Logical Approach by Shiu-Kai Chin and Susan Older, they define a language to describe access control principles throughout the text. By the design of the language, it seemed to be implementable, and so I have.
The language itself has the same operations as propositional logic does with a few additions. Propositional logic is a well used and well studied language, used in artificial intelligence research to verify mathematical proofs and to determine other true statements from a set of true statements. One specific example of a language that relates itself to first-order logic, an expansion upon the idea of propositional logic, is Prolog. Prolog is unique from most other languages is that it is a declarative language. All of the statements in Prolog are either facts, true statements or statically initialized data, or rules, statements that define relations about facts, to form a knowledge base. Prolog is used by querying things about the knowledge base by resolving statements in the knowledge base to satisfy the query. Since Prolog seems to have the same objective as the language defined in the book, I decided to base my implementation on the same kind of concept.
To start writing the language, I must use another language. Since the problem seems to be a very mathematical / computer science-y problem, I decided to use a functional language, Scheme. Scheme is a derivative of Lisp and is the functional language I have the most experience with. The first step to write the language is to define how it is going to written by the user and interpreted by the computer, and that is through the design of the lexer and the parser. The lexer is the part that pulls out symbols from the text input, and the parser verifies that the symbols are in the right order by the definition of the grammar. For the lexer, permissions, are recognized as words that start with a lowercase letter and principal names start with an uppercase letter. In the book, the grammar has already been laid out.
Princ: PName / Princ & Princ / Princ | Princ
The parentheses around most of the terms aren’t needed because an operator precedence is laid out as well. However writing the parser to accept this with optional parenthesis, enforce the operator precedence, as well as being able to be typed without special symbols, I have to mangle the grammar a bit.
Comp: ImpForm / Comp == ImpForm
ImpForm: OrForm / ImpForm -> OrForm
OrForm: AndForm / OrForm || AndForm
AndForm: ACForm / AndForm ^ ACForm
ACForm: NegForm / Princ says NegForm / Princ controls NegForm / Princ reps Princ on NegForm
NegForm: !NegForm / Simple
Simple: PropVar / ( form )
Princ: SimPrinc / SimPrinc & Princ / SimPrinc | Princ
SimPrinc: PName / ( SimPrinc )
The thing to note that differentiates this language from propositional logic is the inclusion of the conjunction ( & ), quoting ( | ), says, controls, speaks for (=>), and reps/on operators, used for describing access control. Says is the operator mainly used for queries and requests that a certain principal requests access to a resource. “Speaks for” is used for trust assumptions between two principals. Controls is the statement that defines control over a resource, and reps/on is used in delegation. As defined in the book, controls and reps/on is merely syntactic sugar. The statement “X controls Y” is broken into “(X says Y) -> Y”, and the statement “X reps Y on Z” is expanded to “(X says (Y says Z)) -> (Y says Z)”. Logical implication and congruence are also broken down into their definitions. Conjunction and quoting are operators that only occur within says statements and are dealt with a little later on.
The parser creates the statements into a binary tree of operations. Those operations at this point only include not, and, or, conjunction, quoting, says, and speaks for. Aside from the new access control operators, this is perfect for resolving sets of statements. However, they do need to be in a form called conjunctive normal form (CNF) for the resolution to go smoothly. Conjunctive normal form a form where literals (such as names, variables, access control statements, and negations of the others) are or-ed together to form clauses, and where those clauses are then and-ed together. The knowledge base that we are building is assumed to be a collection of clauses and-ed together, so when the statements are converted to CNF, any first-level ands are made to be two separate statements in the knowledge base. A few quirks in my CNF conversion function (to-cnf in the source) are the reduction of double negation, and the expansion of the quoting and conjunction operators. Specifically, quoting and conjunction are defined by two different axioms in chapter 3 of the book. Quoting resolves a statement like “A | B says C” to “A says (B says C)”, and conjunction resolves “A & B says C” to “A says C ^ B says C”. Effectively, these two operations are eliminated before the resolution begins.
Resolution is how the knowledge base arrives at an answer. When we query the knowledge base the says statement (query) and the negation of the permission are put in the knowledge base. This comes in handy for how resolution works. Resolution works by eliminating two contradicting literals in the knowledge base. So first, the all of the literals in the knowledge base are aggregated. Then, the first literal is taken and the rest of the list is searched for the negative of that literal. If it is found, it is removed from the list and the search continues. If it is not found, the literal goes into a leftover pile to be searched later. If the query is in the leftover pile, that means it has not been eliminated and permission has not been granted. The negation of the permission is important to insert since it would get eliminated if the query is eliminated, because of how the controls is just an implication of a says statement to the permission. Through this method, the interpreter can determine if a permission is granted or denied.
The main method in the interpreter is called access-check. Access-check takes a filename, a “user”, and a permission name. In reality, the “user” is just a statement in the form of Princ from the grammar. The filename that it takes should be a file with a series of statements that form the rules of the reference monitor. Example 5-1 from the book makes a pretty good example of discretionary access control for the interpreter:
Susan says (Bill controls readfoo)
Susan says (Bill controls writefoo)
Susan says (Carla controls execfoo)
Susan controls (April controls readfoo)
Susan controls (Bill controls readfoo)
Susan controls (Bill controls writefoo)
Susan controls (Carla controls execfoo)
The other arguments that follow would be “Carla” for the user and “execfoo” for the permission to get a “Granted” message. Right now, Susan doesn’t have the ability to change the permissions to foo since the knowledge base is hand-written. However, with a good wrapper around this base system, Susan should be able to modify the file that modifies the permissions for foo. But as the interpreter stands now, it is great for mandatory access control since all of the permissions are static.
Another thing to demonstrate is delegation. Example 7-4 from the book also translates well to the interpreter:
Beth controls acceptRafflePrize
The other arguments would be “Dawn | Beth” and “acceptRafflePrize”. Quoting and conjunction statements are allowed as the “user”. This leads to a quirk that I found in my testing of the interpreter. The “user” allowed any other type of statement to be included with it! Therefore I could inject my own facts into the knowledge base by using “otherFact ^ Dawn” and it would interpret the query as “otherFact ^ (Dawn says permission)” which would then split “otherFact” and “Dawn says permission” into separate statements in the knowledge base. I locked this down by only allowing “says” statements to be searched on in the search-kb function which initializes the process of resolution.
As far as the performance of the interpreter, big-O on access-check is mainly determined by the CNF conversion in the function to-cnf and becomes O(2^n) where n is the number of literals. This is because the worst case is when the statement is a series of disjunctions of conjunctions of literals rather than conjunctions of disjunctions of literals like CNF expects. However, this rarely occurs, since most of the statements produce implications which are converted to single disjunctions. As far as real-world time, I tested the interpreter with a 104 statement input file, and the average time across 10 runs was 0.444 seconds. As far as my thoughts on the language, I think it would be clunky to write permissions in this kind of syntax. Also, it doesn’t seem fast enough to produce timely results. Maybe with some improvements to the interpreter, the language would be bearable, but as it is now, I do not think there will be new systems based around this language. It is great for proofs but translating it to code is awkward.
I used Racket Scheme and the source with examples is available at github.com/RaineForest/BookLang.