Documentation
¶
Overview ¶
Package auth supports Tao authorization and authentication, primarily by defining and implementing a logic for describing principals, their trust relationships, and their beliefs.
The grammar for a formula in the logic is roughly:
Form ::= Term [from Time] [until Time] says Form
| Term speaksfor Term
| forall TermVar : Form
| exists TermVar : Form
| Form implies Form
| Form or Form or ...
| Form and Form and ...
| not Form
| Pred | false | true
Quantification variables range over Terms.
TermVar : Identifier
Times are integers interpreted as 64-bit unix timestamps.
Time ::= int64
Predicates are like boolean-valued pure functions, with a name and zero or more terms as arguments.
Pred ::= Identifier(Term, Term, ...)
| Identifier()
Terms are concrete values, like strings, integers, or names of principals.
Term ::= Str | Bytes | Int | Prin | PrinTail | TermVar
Int can be any Go int. Str is a double-quoted Go string. Bytes is written as pairs of hex digits, optionally separated by whitespace, between square brackets. Bytes can also be written as base64w without whitespace between curly braces.
Principal names specify a key or a tpm, and zero or more extensions to specify a sub-principal of that key.
PrinType ::= key | tpm
Prin ::= PrinType(Term)
| PrinType(Term).PrinExt.PrinExt...
PrinExt ::= Identifier(Term, Term, ...)
| Identifier()
Principal tails represent a sequence of extensions that are not rooted in a principal. They are used to make statements about authorized extensions independent of the root principal. For example, they are used to specify that a given program is authorized to execute on any platform. A PrinTail must be followed by at least one extension.
PrinTail ::= ext.PrinExt.PrinExt...
Identifiers for predicate and principal extension names and quantification variables are limited to simple ascii printable identifiers, with inital upper-case, and no punctuation except '_':
PredName ::= [A-Z][a-zA-Z0-9_]* ExtName ::= [A-Z][a-zA-Z0-9_]*
The keywords used in the above grammar are:
from, until, says, speaskfor, forall, exists, implies, or, and, not, false, true, key
The punctuation used are those for strings and byte slices, plus:
'(', ')', ',', '.', ':'
It is possible to represent nonsensical formulas, so some sanity checking may be called for. For example, in general:
- The left operand of Says should be Prin or TermVar, as should both operands of Speaksfor.
- All TermVar variables should be bound.
- Conjunctions should have at least one conjunct.
- Disjunctions should have at least one disjunct.
- Identifiers should be legal using the above rules.
- The parameter for key() should be TermVar or Bytes.
Specific applications may impose additional restrictions on the structure of formulas they accept.
All of the above elements have three distinct representations. The first representation is ast-like, with each element represented by an appropriate Go type, e.g. an int, a string, or a struct containing pointers (or interfaces) for child elements. This representation is meant to be easy to programmatically construct, split apart using type switches, rearrange, traverse, etc.
The second representation is textual, which is convenient for humans but isn't canonical and can involve tricky parsing. When parsing elements from text:
Whitespace is ignored between elements (except around the suprincipal dot operator, and before the open paren of a Pred, Prin, or, PrinExt); For binary operators taking two Forms, the above list shows the productions in order of increasing precedence; In all other cases, operations are parsed left to right; Parenthesis can be used for specifying precedence explicitly.
When pretty-printing elements to text, a single space is used before and after keywords, commas, and colons. Elements can also be pretty-printed with elision, in which case keys and long strings are truncated.
The third representation is an encoded sequence of bytes. This is meant to be compact, relatively easy to parse, and suitable for passing over sockets, network connections, etc. The encoding format is custom-designed, but is roughly similar to the format used by protobuf.
Several alternative encodings were considered:
Protobuf encoding with protobuf definitions: This would require either duplicating all Form and Term types as proto definitions, then writing conversion and validation code. The encoding would likely not be space efficient, and it would be essentially Tao's only hard dependency on protobuf. Protobuf encoding with hand-written encoding/decoding: The goprotobuf library currently lacks good support for this. Also, protobuf allows encoded data to be shuffled, making decoding much more complicated than necessary. encoding/gob: Not language-agnostic. The self-describing datatype encoding scheme is probably overkill as well. strings using textual representation of Form and Term elements: This pulls into all TCB a somewhat complex lexer and parser. The encoding is also not space efficient.
The encoding we use instead is meant to be conceptually simple, reasonably space efficient, and simple to decode. And unlike most of the other schemes agove, strictness rather than flexibility is preferred. For example, when decoding a Form used for authorization, unrecognized fields should not be silently skipped, and unexpected types should not be silently coerced.
Each element is encoded as a type tag followed by encodings for one or more values. The tag is encoded as a plain (i.e. not zig-zag encoded) varint, and it determines the meaning, number, and types of the values. Values are encoded according to their type:
An integer or bool is encoded as plain varint. A string is encoded as a length (plain varint) followed by raw bytes. A pointer is encoded the same as a boolean optionally followed by a value. Variable-length slices (e.g. for conjuncts, disjuncts, predicate arguments) are encoded as a count (plain varint) followed by the encoding for the each element. An embedded struct or interface is encoded as a tag and encoded value.
Differences from protobuf:
Our tags carry implicit type information. In protobuf, the low 3 bits of each tag carries an explicit type marker. That allows protobuf to skip over unrecognized fields (not a design goal for us). It also means protobuf can only handle 15 unique tags before overflowing to 2 byte encodings. Our tags describe both the meaning and the type of all enclosed values, and we use tags only when the meaning or type can vary (i.e. for interface types). Protobuf uses tags for every enclosed value, and those tags also carry type information. Protobuf is more efficient when there are many optional fields. For us, nearly all fields are required. Enclosed values in our encoding must appear in order. Protobuf values can appear in any order. Protobuf encodings can concatenated, truncated, etc., all non-features for us.
Note: In most cases, a tag appears only when the type would be ambiguous, i.e. when encoding Term or Form.
Index ¶
- Variables
- func Marshal(e LogicElement) []byte
- func SubprinOrIdentical(child, parent Term) bool
- type And
- type AnyForm
- type AnyTerm
- type Buffer
- type Bytes
- type Const
- type Exists
- type Forall
- type Form
- type Implies
- type Int
- type LogicElement
- type Not
- type Or
- type Pred
- type Prin
- type PrinExt
- type PrinTail
- type Says
- type Speaksfor
- type Str
- type SubPrin
- type Term
- type TermVar
- Bugs
Constants ¶
This section is empty.
Variables ¶
var ElisionCutoff int = 32
ElisionCutoff is the maximum length a String or Byte can be without being elided.
var ElisionLength int = 24
ElisionLength is the number of characters to show in an elided String or Byte.
Functions ¶
func SubprinOrIdentical ¶
SubprinOrIdentical checks whether child is a subprincipal of parent or is identical to parent.
Types ¶
type And ¶
type And struct {
Conjunct []Form
}
And conveys formula "Conjunct[0] and Conjunct[1] and ... and Conjunct[n]"
func (And) ShortString ¶
ShortString returns an elided pretty-printed And.
type AnyForm ¶
type AnyForm struct {
Form Form
}
AnyForm is a struct that can be used in when scanning for a Form, since Form itself is an interface and interface pointers are not valid receivers. TODO(kwalsh) Can this be accomplished with a pointer to interface?
func (*AnyForm) Scan ¶
Scan parses a Form, with optional outer parens. This function is not greedy: it consumes only as much input as necessary to obtain a valid formula. For example, "(p says a and b ...)" and "p says (a and b ...) will be parsed in their entirety, but given "p says a and b ... ", only "p says a" will be parsed.
type AnyTerm ¶
type AnyTerm struct {
Term Term
}
AnyTerm is a struct that can be used in when scanning for a Term, since Term itself is an interface and interface pointers are not valid receivers. TODO(kwalsh) Can this be accomplished with a pointer to interface?
type Buffer ¶
type Buffer struct {
// contains filtered or unexported fields
}
Buffer holds partially encoded or decode auth elemnts. Note: We could do capacity-doubling, etc., but we favor simplicity for now.
func (*Buffer) DecodeBool ¶
DecodeBool calls DecodeVarint then converts the result to a bool.
func (*Buffer) DecodeString ¶
DecodeString decodes a string, shrinking the buffer.
func (*Buffer) DecodeVarint ¶
DecodeVarint decodes an int, shrinking the buffer.
func (*Buffer) EncodeBool ¶
EncodeBool converts b to an int then calls EncodeVarint.
func (*Buffer) EncodeString ¶
EncodeString encodes a string as a length and byte array, growing the buffer.
func (*Buffer) EncodeVarint ¶
EncodeVarint encodes an int as a (non zig-zag) varint, growing the buffer.
type Bytes ¶
type Bytes []byte
Bytes is a byte slice used as a Term.
func (Bytes) ShortString ¶
ShortString returns a pretty-printed Bytes.
type Const ¶
type Const bool
Const conveys formula "true" or formula "false"
func (Const) ShortString ¶
ShortString returns an elided pretty-printed Const.
type Exists ¶
Exists conveys formula "(exists Var : Body)" where Var ranges over Terms.
func (*Exists) Scan ¶
Scan parses an Exists, with optional outer parens. This function is not greedy.
func (Exists) ShortString ¶
ShortString returns an elided pretty-printed Exists.
type Forall ¶
Forall conveys formula "(forall Var : Body)" where Var ranges over Terms.
func (*Forall) Scan ¶
Scan parses a Forall, with optional outer parens. This function is not greedy.
func (Forall) ShortString ¶
ShortString returns an elided pretty-printed Forall.
type Form ¶
type Form interface {
LogicElement
// contains filtered or unexported methods
}
Form is a formula in the Tao authorization logic.
type Implies ¶
Implies conveys formula "Antecedent implies Consequent"
func (*Implies) Scan ¶
Scan parses an Implies, with required outer parens. This function is not greedy.
func (Implies) ShortString ¶
ShortString returns an elided pretty-printed Implies.
type Int ¶
type Int int
Int is an int used as a Term.
func (Int) ShortString ¶
ShortString returns an elided pretty-printed Int.
type LogicElement ¶
type LogicElement interface {
// Marshal writes a binary encoding of the element into b.
Marshal(b *Buffer)
// String returns verbose pretty-printing text for the element.
String() string
// ShortString returns short debug-printing text for the element.
ShortString() string
// fmt.Formatter is satisfied by all elements. Using format %v will result in
// verbose pretty-printing, using format %s will result in short
// debug-printing, and other formats will use an unspecified format.
fmt.Formatter // Format(out fmt.State, verb rune)
// contains filtered or unexported methods
}
LogicElement is any element of the authorization logic, i.e. a formula, a term, or a principal extension.
type Not ¶
type Not struct {
Negand Form
}
Not conveys formula "not Negand"
func (Not) ShortString ¶
ShortString returns an elided pretty-printed Not.
type Or ¶
type Or struct {
Disjunct []Form
}
Or conveys formula "Disjunct[0] or Disjunct[1] or ... or Disjunct[n]"
func (Or) ShortString ¶
ShortString returns an elided pretty-printed Or.
type Pred ¶
Pred is a predicate, i.e. a boolean-valued (pure) function.
func MakePredicate ¶
MakePredicate creates a predicate with the given name and arguments. Arguments can be Prin, Int (or integer types that be coerced to it), Str (or string), or PrinTail. Anything else is coerced to Str.
func (Pred) ShortString ¶
ShortString returns an elided pretty-printed Pred.
type Prin ¶
type Prin struct {
Type string // The keyword of a principal token, e.g. "key" or "tpm".
KeyHash Term // TermVar or Bytes with hashed CryptoKey protobuf structure with purpose CryptoKey.VERIFYING. Or this can be a hashed marshalled TPM AIK, or a X.509 certificate, marshalled as ASN.1 DER then hashed.
Ext SubPrin // zero or more extensions for descendents
}
Prin uniquely identifies a principal by a public key, used to verify signatures on credentials issued by the principal, and a sequence of zero or more extensions to identify the subprincipal of that key.
func NewKeyPrin ¶
NewKeyPrin returns a new Prin of type "key" with the given key material.
func NewTPM2Prin ¶
NewTpm2Prin returns a new Prin of type "tpm2" with the given (ek) key material.
func NewTPMPrin ¶
NewTpmPrin returns a new Prin of type "tpm" with the given (aik) key material.
func UnmarshalPrin ¶
UnmarshalPrin decodes a Prin.
func (Prin) MakeSubprincipal ¶
MakeSubprincipal creates principal p.e... given principal p and extensions e.
func (Prin) ShortString ¶
ShortString returns an elided pretty-printed Prin.
type PrinExt ¶
PrinExt is an extension of a principal.
func UnmarshalPrinExt ¶
UnmarshalPrinExt decodes a PrinExt.
func (PrinExt) ShortString ¶
ShortString returns an elided pretty-printed PrinExt.
type PrinTail ¶
type PrinTail struct {
Ext SubPrin // one or more extensions
}
A PrinTail is a Term that represents a free-floating sequence of PrinExt values. It represents the tail of a list of Prin extensions. Its textual representation always starts with the keyword "ext".
func UnmarshalPrinTail ¶
UnmarshalPrinTail decodes a PrinTail.
func (PrinTail) ShortString ¶
ShortString returns an elided pretty-printed PrinTail.
type Says ¶
type Says struct {
Speaker Term
Time *int64 // nil to omit
Expiration *int64 // nil to omit
Message Form
}
Says conveys formula "Speaker from Time until Expiration says Message"
func (Says) ShortString ¶
ShortString returns an elided pretty-printed Says.
type Speaksfor ¶
Speaksfor conveys formula "Delegate speaksfor Delegator"
func (*Speaksfor) Scan ¶
Scan parses a Speaksfor, with optional outer parens. This function is not greedy.
func (Speaksfor) ShortString ¶
ShortString returns an elided pretty-printed Speaksfor.
type Str ¶
type Str string
Str is a string used as a Term.
func (Str) ShortString ¶
ShortString returns an elided pretty-printed Str.
type SubPrin ¶
type SubPrin []PrinExt
SubPrin is a series of extensions of a principal.
func UnmarshalSubPrin ¶
UnmarshalSubPrin decodes a SubPrin.
func (SubPrin) ShortString ¶
ShortString returns an elided pretty-printed SubPrin.
type Term ¶
type Term interface {
LogicElement
Identical(other Term) bool
// contains filtered or unexported methods
}
Term is an argument to a predicate or a principal extension.
type TermVar ¶
type TermVar string
TermVar is a term-valued variable.
func (TermVar) ShortString ¶
ShortString returns an elided pretty-printed TermVar.
Notes ¶
Bugs ¶
fmt.ScanState.ReadRune() returns incorrect length. See issue 8512 here: https://code.google.com/p/go/issues/detail?id=8512
Source Files