capDL-tool/doc/capDL.md - 3p/sel4/capdl - Git at Google

 <!--
      Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)

      SPDX-License-Identifier: CC-BY-SA-4.0
 -->

 <!-- title: capDL Language Specification -->

 This document defines capDL revision 1.0, a language for capability
 distributions.

 # Background and Purpose

 The purpose of capDL is describing snapshots of a system running on the
 seL4 microkernel. In particular, it can be used to describe which
 entities have access to which seL4 capabilities.

 The main objectives are to use these descriptions for specifying
 systems, for security analysis of systems, as input for automated
 bootstrapping of systems, and for debugging applications running on
 seL4. A capDL specification can be complete, i.e. give a full picture of
 all capabilities in the system, or the system can be underspecified,
 showing only the capabilities accessible to a particular component. It
 is possible to describe system states in capDL that are not reachable
 via actual system executions. It is also possible to leave out details
 in a system specification that for instance are not important for a
 security analysis (e.g. because the relevant authority is already
 represented otherwise), but that would be necessary for an actual
 implementation of the system.

 # Syntax

 This section gives a complete definition of the capDL syntax in BNF.

 ## Lexical Tokens

 The lexical tokens of capDL are numbers (`number`), identifiers
 (`identifier`), and verbatim symbols and operators typeset between
 quotes `”` in the syntax section below.

 Numbers are in decimal, hexadecimal (with prefix 0x), or octal (with
 prefix 0) form. Identifiers start with a letter `[a-zA-Z]`, followed by
 a sequence of letters `[a-zA-Z]`, numbers `[0-9]`, the underscore
 character `_`, or a `@` character.

 The language is case sensitive.

 Comments can occur between any two tokens and can be nested. A
 potentially multiline comment starts with the two characters `/*` and
 ends with `*/`. A one-line comment starts with `–`. All characters after
 `–` up to the end of the same line are ignored.

 Whitespace (a sequence of space, newline and tab characters) can occur
 between any two tokens and is ignored.

 ## Syntax

 This section describes the concrete syntax of capDL using the tokens
 defined above. The main syntactic entity of a file is `module` defined
 in section [Modules](#modules).

 ### Names and Ranges

       name ::= identifier

       num ::= '[' number ']'
       range ::= number '..' number  | '..' number  | number  '..' | number
       ranges ::=  '[' ']' | '[' range (',' range)* ']'

       name_ref ::= name ranges?
       qname ::= name_ref ('/' name_ref)*

 ### Object Declarations

       obj_decls ::= 'objects' '{' obj_decl* '}'

       obj_decl ::= qname '=' object

       object ::= object_type object_params? opt_obj_decls?

       object_type ::= 'ep'  | 'notification' | 'tcb' | 'cnode' | 'ut' | 'irq' |
                       'asid_pool' | 'pt' | 'pd' | 'frame' | 'io_ports' |
                       'io_device' | 'io_pt' | 'vcpu'

       object_params ::= '(' (object_param (',' object_param)*)? ')'

       object_param   ::= obj_bit_size | obj_vm_size | io_pt_level | obj_ports_size |
                          init_arguments | tcb_dom | obj_paddr | domain_id |
                          pci_device
       obj_bit_size   ::= number 'bits'
       obj_vm_size    ::= number ('k' | 'M')
       io_pt_level    ::= 'level' ':' number
       obj_ports_size ::= number 'k' 'ports'
       init_arguments ::= 'init' ':' '[' (number (',' number)*)? ']'
       tcb_dom        ::= 'dom' ':' number
       obj_paddr      ::= 'paddr' ':' number
       domain_id      ::= 'domainID' ':' number
       pci_device     ::= number ':' number '.' number

       opt_obj_decls ::= '{' ((obj_decl | name_ref) ','?)* '}'

 ### Capability Declarations

       cap_decls ::= 'caps' '{' (cap_name_decl | cap_decl)* '}'

       cap_name_decl ::= name '=' '(' name_ref ',' slot ')'

       slot ::= number | symbolic_slot
       symbolic_slot ::= 'cspace' | 'vspace' | 'reply_slot' | 'caller_slot' |
                         'ipc_buffer_slot'

       cap_decl ::= name_ref '{' (cap_mapping_or_ref ';'?)* '}'

       cap_mapping_or_ref ::= (slot ':')? cap_name? (cap_mapping | cap_name_ref)

       cap_name    ::= name_ref '='
       cap_mapping ::= name_ref cap_params? parent?
       cap_params  ::= '(' cap_param (',' cap_param)* ')'

       cap_param ::= right+
                   | 'masked' ':' right+
                   | 'guard' ':' number
                   | 'guard_size' ':' number
                   | 'badge' ':' number
                   | 'ports'  ':' ranges
                   | 'reply'
                   | 'master_reply'
                   | 'asid' ':' asid
                   | 'cached'
                   | 'uncached'

       right ::= 'R' | 'W' | 'G' | 'X'
       asid ::= '(' number ',' number ')'

       parent ::= '- child_of' slot_ref

       slot_ref ::= '(' name_ref ',' slot ')' | name_ref

       cap_name_ref ::= '<' name_ref '>' cap_params? parent?

 ### IRQ Declarations

       irq_decls ::='irq_maps' '{' (irq_mapping ';'?)* '}'

       irq_mapping ::= (number ':')? name_ref

 ### CDT Declarations

       cdt_decls ::='cdt' '{' cdt_decl* '}'

       cdt_decl ::= slot_ref '{' ((slot_ref | cdt_decl) ';'?)* '}'

 ### Modules

       arch ::= 'arch' ('ia32' | 'arm11')

       module ::= arch (obj_decls | cap_decls | irq_decls | cdt_decls)+

 # Semantics

 In this section we show the semi-formal semantics of capDL in the form
 of its underlying data model in Haskell and give a brief rationale for
 its contents. This data model can be made fully formal by mapping it
 directly into the Isabelle theorem prover via Data61's existing
 Haskell-to-Isabelle translation tool. The data model can also be mapped
 into various output formats.

 After describing the data model below, we outline a semi-formal
 definition of the semantics: mapping the capDL syntax into the capDL
 data model.

 ## Data Model

 ### Rationale
 The purpose of capDL is describing a snapshot of the capability
 distribution in a system running on the seL4 microkernel. For this
 purpose, we need to know which objects exist in the system and which
 capabilities they have access to. The second purpose of capDL is to
 serve as sufficiently detailed input to automated code generation
 tools. Therefore we need to include all information about capability
 arguments that such implementations will need. Some of this information
 will not be relevant for security analysis. For instance, for a
 security analysis it may be necessary to know which frames of physical
 memory an entity in the system can access via virtual memory, but it is
 not necessary to know under which virtual address each of these
 physical addresses is visible to the process. For a concrete
 implementation of a bootstrapping component on the other hand, this
 latter information is crucial.

 ### The Model

 We refer to objects by name. This name could be of any type; for
 convenience we either use a plain string or a string with an index. We
 use the `Maybe` type of Haskell to express this.

     types ObjID = (String, Maybe Word)

 With this the capability state of a system is fully described by a map
 from `ObjID` to `Object`. Since not all objects and capabilities are
 supported by seL4 on all machine architectures, we also store which
 architecture the system is intended for.

     data Model =  Model {
                       arch :: Arch,
                       objects :: Map ObjID Object
                   }

     data Arch = IA32 | ARM11

 Objects are described by the following data type. We are mainly
 interested in what capabilities an object contains. We also store
 information that is relevant for creating an object such as its type and
 its size when the size is configurable. This means in contrast to the
 security model, where we only talk about abstract entities, we give more
 detailed information in capDL.

     types CapMap = Map Word Cap

     data Object = Endpoint
                 | Notification
                 | TCB { slots :: CapMap, initArguments :: [Word] }
                 | CNode { slots :: CapMap, sizeBits :: Word }
                 | Untyped { maybeSizeBits :: Maybe Word }

                 | ASIDPool { slots :: CapMap }
                 | PT { slots :: CapMap }
                 | PD { slots :: CapMap }
                 | Frame { vmSizeBits :: Word }
                 | IOPorts { size :: Word }
                 | IOPT { slots :: CapMap, level :: Word }
                 | IODevice { slots :: CapMap }

 The first two objects, communication endpoints and notifications, do not
 store any capabilities and have a fixed size. Thread Control Blocks
 (TCB) contain a small number of capability registers, modelled by the
 field `slots`, a map from a machine word (the slot/register number) to
 the capability that is stored in that slot. Slots may be empty. CNode
 objects are the main capability storage object in seL4. They have
 configurable size. Untyped objects are conceptual containers for
 dynamically created objects. They cover a set of objects referred to by
 their `ObjID`. This set is called the covering set. In the
 implementation untyped objects must have a size, but in capDL
 specifications we often want to leave the size unspecified (as large as
 necessary).

 The next batch of objects in the data type above are architecture
 dependent. Most of these data structures and devices do not store actual
 capabilities in the kernel and hardware implementation. Instead they
 store pointers or mappings to other resources in the system. Since these
 resources are already represented as objects, we use capabilities to
 model these mappings and to express the access, for instance, a device
 may have to physical memory. In detail, the architecture dependent
 objects are as follows. ASID pools store which page directories (PD) can
 be activated by the machine. As mentioned, we represent this mapping as
 a capability in the model. Analogously, we model the mappings in virtual
 memory objects page directory (PD) and page table (PT). Physical memory
 frames (`Frame`) come in different sizes, depending on architecture, but
 do not contain further capabilities. IOMMU page tables (`IOPT`) come in
 multiple levels and again store mappings to frames or further page
 tables. Finally, hardware devices are represented by the object type
 `IODevice`. Again, we model the access hardware may have to resources in
 the system as capabilities. Specifically, IODevices may have a
 capability to a CNode for IRQ delivery, potentially multiple
 capabilities to physical memory frames for memory mapped device
 registers, and one capability for the root IOMMU space.

 To conclude the description of the capDL data model, it remains to
 define the data type of capabilities `Cap`. Almost all capabilities in
 seL4 refer to one specific object. Some may refer to a set of objects or
 implicitly to all objects of a given type. Many of the capabilities
 store explicit access rights. These are modelled as follows:

     data Rights = Read | Write | Grant | GrantReply
     types CapRights = Set Right

 Again in contrast to the security model of seL4, we explicitly
 distinguish different types of capabilities in capDL and store slightly
 different kinds of additional information with each. As a side effect,
 we do not need an explicit representation of the create right. The
 create right is conferred by the possession of an untyped capability.

     data Cap = NullCap
              | UntypedCap { capObj :: ObjID }
              | EndpointCap { capObj :: ObjID, capBadge :: Word,
                              capRights :: CapRights }
              | NotificationCap { capObj :: ObjID, capBadge :: Word,
                                  capRights :: CapRights }
              | ReplyCap { capObj :: ObjID }
              | MasterReplyCap { capObj :: ObjID }
              | CNodeCap { capObj :: ObjID, capGuard :: Word,
                           capGuardSize :: Word }
              | TCBCap { capObj :: ObjID }
              | IRQControlCap
              | IRQHandlerCap { capObj :: ObjID }
              | FrameCap { capObj :: ObjID, capRights :: CapRights }
              | PTCap { capObj :: ObjID }
              | PDCap { capObj :: ObjID }
              | ASIDControlCap
              | ASIDPoolCap { capObj :: ObjID }
              | IOPortsCap { capObjs :: Set Word }
              | IOSpaceMasterCap
              | IOSpaceCap { capObj :: ObjID }
              | IOPTCap { capObj :: ObjID }

 In detail, the capabilities are as follows. We go through the list of
 capabilities and give a brief indication of the authority they convey.
 The `NullCap` is occasionally used to represent the absence of a
 capability. An untyped capability points to an untyped object and
 confers the right to issue create/retype and revoke/delete operations.
 Endpoint and notification capabilities point to their respective object
 types. They explicitly store which Read/Write/Grant access is conferred
 to the communications channel and they may carry one machine word of
 additional information, called the badge. CNode capabilities in addition
 to their CNode object reference carry information that influences the
 lookup of capabilities in the node they point to. This information
 consists of a guard in the sense of guarded page tables, the size of
 that guard, and finally the rights to the CNode object itself. A TCB cap
 gives authority over one TCB object with given access rights. The
 IRQControl capability gives authority to create specific IRQHandler
 capabilities. Each device may have a special CNode associated with it
 that may contain a notification which in turn is used to deliver
 interrupts to user level. IRQHandler caps in capDL point to these
 specific CNodes. It confers the authority to change which endpoint the
 interrupt is delivered to. Frame capabilities confer authority to map
 and unmap physical memory frames into and from a page directory or page
 table with the specified access rights. PT caps give authority to
 map/unmap page tables into/from page directories and PD caps give the
 authority to map/unmap page directories into ASID pools and to install
 them as virtual memory space of a process. The ASIDControlCap together
 with an Untyped cap confers authority to create new ASID pools. Only a
 limited, fixed number can be created in the system. ASIDPool caps give
 the authority to map/unmap page directories into/from the ASID pool.
 Mapping a frame into a page table for instance, needs the frame cap to
 specify which frame to map with which rights and the PT cap to specify
 in which page table. The IOPorts capability gives access to a set of
 IOPorts on the ia32 architecture. The IOSpaceMasterCap confers the
 authority to create IOSpace caps for specific devices. IOSpaceCaps point
 to IODevices and confer the authority to set the root IOPageTable for
 that device. IOPTCaps are the IOMMU analogue to PT and PD caps in normal
 virtual memory.

 ## Semantics

 In this section, we define a mapping from the syntax of capDL to the
 data model of capDL. The mapping is defined by going over the relevant
 productions in the capDL grammar and describing the corresponding model.

 ### Names and Ranges

       name ::= identifier

 Names are mapped to `ObjID`s in the model. A name without index maps to
 `(name, Nothing)`. Qualified names will be defined in the object
 declaration section.

       num ::= '[' number ']'

 This production maps to a single index and is used to either declare a
 set of objects, in which case the number is the number of objects, or to
 refer to a specific index. The term name\[x\] maps to the `ObjID`
 `(name, Just x)`.

       range ::= number '..' number  | '..' number  | number  '..' | number
       ranges ::=  '[' ']' | '[' range (',' range)* ']'
       name_ref ::= name ranges?

 Ranges stand for sets of `ObjID`s. For a set declared as `name[n]`, the
 following mappings apply:

 -   `name[..b]` refers to `name[0]`, `name[1]`, .., `name[b]`

 -   `name[a..]` refers to `name[a]`, `name[a+1]`, .., `name[n]`

 -   `name[a..b]` refers to `name[a]`, `name[a+1]`, .., `name[b]`

 -   `name[]` refers to `name[0]`, `name[1]`, .., `name[n]`

 A list of ranges `name[r1,r2,..r3]` refers to the union of the ranges
 `name[r1]`, `name[r2]`, .., `name[r3]`.

 ### Module

       arch ::= 'arch' ('ia32' | 'arm11')
       module ::= arch (obj_decls | cap_decls)+

 A module maps to a full `Model` in the data model. Its `Arch` component
 is determined by `arch`, its mapping from `ObjID` to `Object` by the
 object and capability declarations described below.

 ### Object Declarations

       obj_decls ::= 'objects' obj_decl*

 An object declaration section defines a set of objects. Each object name
 of typed objects should be declared only once. The covering set of
 untyped objects may be declared multiple times. The total covering set
 is the union of all covering sets mentioned for that object.

       obj_decl ::= qname '=' object

 An object declaration has a potentially qualified name and dimension on
 the left hand side and an object content declaration on the right hand
 side. A qualified name `name1/name2/name3[n]` implicitly declares the
 untyped objects `name1` and `name2`. It also declares that `name2` is
 covered by `name1` and `name3` covered by `name2`. Giving a dimension
 `[n]` means that n objects `(name3, Just 0)` to `(name3, Just (n-1))`
 are declared, each with the same content described on the right hand
 side of the equation.

 The right hand side is defined by the following syntax productions:

       object ::= object_type object_params? obj_decls?

       object_type ::= 'ep'  | 'notification' | 'tcb' | 'cnode' | 'ut' |
                       'asid_pool' | 'pt' | 'pd' | 'frame' | 'io_ports' |
                       'io_device' | 'io_pt'

       object_params ::= '(' object_param (',' object_param)* ')'

       object_param   ::= obj_bit_size | obj_vm_size | io_pt_level | obj_ports_size
       obj_bit_size   ::= number 'bits'
       obj_vm_size    ::= number ('k' | 'M')
       io_pt_level    ::= 'level' ':' ('1' | '2' | '3')
       obj_ports_size ::= number 'k' 'ports'

       obj_decls ::= '{' ((obj_decl | name_ref) ','?)* '}'

 The object content is given by the type of the object mapping to its
 corresponding object type in the data model. Some of the object types in
 the model require a size parameter, given in bits (where n bits means a
 size of 2^n entries). Frames' sizes are specified directly as are the
 levels of IOMMU page tables. Untyped objects can be followed by a nested
 object declaration. Writing

     name1 = ut {
       name2/name3 [n] = object
       name2/name4 = object
      ...
     }

 is equivalent to writing

     name1/name2/name3 [n] = object
     name1/name2/name4 = object
     ...

 ### Capability Declarations

 The capability content of objects is declared in its own section,
 separately from the list of objects itself.

       cap_decls = 'caps' (cap_name_decl | cap_decl)*

       cap_name_decl ::= name '=' '(' name_ref ',' slot ')'
       slot ::= number | symbolic_slot
       symbolic_slot ::= 'cspace' | 'vspace'

 Next to capability content declarations, there are name declarations for
 capability slots. A capability slot is defined by the container object,
 referred to by a name reference (mapping to a single `ObjID`) and a slot
 inside the container specified by its slot number. The symbolic slot
 names `cspace`, `vspace` stand for slot numbers 0 and 1.

 A capability declaration starts with a set of container objects, each of
 which is declared to contain the capability mappings specified on the
 right hand side. Container objects may occur more than once in a
 specification. Their mappings are the union of all mappings for that
 container object.

       cap_decl ::= name_ref '{' (cap_mapping_or_ref ';'?)* '}'

 A cap mapping is specified by its slot and its capability and
 potentially an inline name declaration for the specified slot in the
 specified container.

       cap_mapping_or_ref ::= slot ':' cap_name? (cap_mapping | cap_name_ref)

       cap_name    ::= name '='
       cap_mapping ::= name_ref cap_params?
       cap_params  ::= '(' cap_param (',' cap_param)* ')'

       cap_param ::= right+
                   | 'masked' ':' right+
                   | 'guard' ':' number
                   | 'guard_size' ':' number
                   | 'irq'
                   | 'badge' ':' number
                   | 'reply'
                   | 'master_reply'

       right ::= 'R' | 'W' | 'G'

       cap_name_ref ::= '<' name_ref '>' cap_params?

 The capability declaration is either a `cap_mapping` or `cap_name_ref`.
 In the latter case the mapping is a copy of the capability in the slot
 referred to by `name` (possibly `masked` with an access rights mask). In
 the former case, a cap is defined by the object it points to, together
 with optional parameters depending on the type of the object in the data
 model. For instance, an endpoint cap is specified if the `ObjID` given
 in the cap declaration refers to an endpoint object. If no parameters
 are mentioned, default parameters are substituted if possible. These
 defaults are: empty set of rights for access rights, full set of rights
 for rights masks, guard 0, guard size 0, and badge 0. The IRQControl cap
 is specified using the reserved `ObjID` `irq_control`, similarly
 ASIDControlCap is specified by `asid_control` and IOSpaceMasterCap by
 `io_space_master`.
	<!--
	Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)

	SPDX-License-Identifier: CC-BY-SA-4.0
	-->

	<!-- title: capDL Language Specification -->

	This document defines capDL revision 1.0, a language for capability
	distributions.

	# Background and Purpose

	The purpose of capDL is describing snapshots of a system running on the
	seL4 microkernel. In particular, it can be used to describe which
	entities have access to which seL4 capabilities.

	The main objectives are to use these descriptions for specifying
	systems, for security analysis of systems, as input for automated
	bootstrapping of systems, and for debugging applications running on
	seL4. A capDL specification can be complete, i.e. give a full picture of
	all capabilities in the system, or the system can be underspecified,
	showing only the capabilities accessible to a particular component. It
	is possible to describe system states in capDL that are not reachable
	via actual system executions. It is also possible to leave out details
	in a system specification that for instance are not important for a
	security analysis (e.g. because the relevant authority is already
	represented otherwise), but that would be necessary for an actual
	implementation of the system.

	# Syntax

	This section gives a complete definition of the capDL syntax in BNF.

	## Lexical Tokens

	The lexical tokens of capDL are numbers (`number`), identifiers
	(`identifier`), and verbatim symbols and operators typeset between
	quotes `”` in the syntax section below.

	Numbers are in decimal, hexadecimal (with prefix 0x), or octal (with
	prefix 0) form. Identifiers start with a letter `[a-zA-Z]`, followed by
	a sequence of letters `[a-zA-Z]`, numbers `[0-9]`, the underscore
	character `_`, or a `@` character.

	The language is case sensitive.

	Comments can occur between any two tokens and can be nested. A
	potentially multiline comment starts with the two characters `/*` and
	ends with `*/`. A one-line comment starts with `–`. All characters after
	`–` up to the end of the same line are ignored.

	Whitespace (a sequence of space, newline and tab characters) can occur
	between any two tokens and is ignored.

	## Syntax

	This section describes the concrete syntax of capDL using the tokens
	defined above. The main syntactic entity of a file is `module` defined
	in section [Modules](#modules).

	### Names and Ranges

	name ::= identifier

	num ::= '[' number ']'
	range ::= number '..' number \| '..' number \| number '..' \| number
	ranges ::= '[' ']' \| '[' range (',' range)* ']'

	name_ref ::= name ranges?
	qname ::= name_ref ('/' name_ref)*

	### Object Declarations

	obj_decls ::= 'objects' '{' obj_decl* '}'

	obj_decl ::= qname '=' object

	object ::= object_type object_params? opt_obj_decls?

	object_type ::= 'ep' \| 'notification' \| 'tcb' \| 'cnode' \| 'ut' \| 'irq' \|
	'asid_pool' \| 'pt' \| 'pd' \| 'frame' \| 'io_ports' \|
	'io_device' \| 'io_pt' \| 'vcpu'

	object_params ::= '(' (object_param (',' object_param)*)? ')'

	object_param ::= obj_bit_size \| obj_vm_size \| io_pt_level \| obj_ports_size \|
	init_arguments \| tcb_dom \| obj_paddr \| domain_id \|
	pci_device
	obj_bit_size ::= number 'bits'
	obj_vm_size ::= number ('k' \| 'M')
	io_pt_level ::= 'level' ':' number
	obj_ports_size ::= number 'k' 'ports'
	init_arguments ::= 'init' ':' '[' (number (',' number)*)? ']'
	tcb_dom ::= 'dom' ':' number
	obj_paddr ::= 'paddr' ':' number
	domain_id ::= 'domainID' ':' number
	pci_device ::= number ':' number '.' number

	opt_obj_decls ::= '{' ((obj_decl \| name_ref) ','?)* '}'

	### Capability Declarations

	cap_decls ::= 'caps' '{' (cap_name_decl \| cap_decl)* '}'

	cap_name_decl ::= name '=' '(' name_ref ',' slot ')'

	slot ::= number \| symbolic_slot
	symbolic_slot ::= 'cspace' \| 'vspace' \| 'reply_slot' \| 'caller_slot' \|
	'ipc_buffer_slot'

	cap_decl ::= name_ref '{' (cap_mapping_or_ref ';'?)* '}'

	cap_mapping_or_ref ::= (slot ':')? cap_name? (cap_mapping \| cap_name_ref)

	cap_name ::= name_ref '='
	cap_mapping ::= name_ref cap_params? parent?
	cap_params ::= '(' cap_param (',' cap_param)* ')'

	cap_param ::= right+
	\| 'masked' ':' right+
	\| 'guard' ':' number
	\| 'guard_size' ':' number
	\| 'badge' ':' number
	\| 'ports' ':' ranges
	\| 'reply'
	\| 'master_reply'
	\| 'asid' ':' asid
	\| 'cached'
	\| 'uncached'

	right ::= 'R' \| 'W' \| 'G' \| 'X'
	asid ::= '(' number ',' number ')'

	parent ::= '- child_of' slot_ref

	slot_ref ::= '(' name_ref ',' slot ')' \| name_ref

	cap_name_ref ::= '<' name_ref '>' cap_params? parent?

	### IRQ Declarations

	irq_decls ::='irq_maps' '{' (irq_mapping ';'?)* '}'

	irq_mapping ::= (number ':')? name_ref

	### CDT Declarations

	cdt_decls ::='cdt' '{' cdt_decl* '}'

	cdt_decl ::= slot_ref '{' ((slot_ref \| cdt_decl) ';'?)* '}'

	### Modules

	arch ::= 'arch' ('ia32' \| 'arm11')

	module ::= arch (obj_decls \| cap_decls \| irq_decls \| cdt_decls)+

	# Semantics

	In this section we show the semi-formal semantics of capDL in the form
	of its underlying data model in Haskell and give a brief rationale for
	its contents. This data model can be made fully formal by mapping it
	directly into the Isabelle theorem prover via Data61's existing
	Haskell-to-Isabelle translation tool. The data model can also be mapped
	into various output formats.

	After describing the data model below, we outline a semi-formal
	definition of the semantics: mapping the capDL syntax into the capDL
	data model.

	## Data Model

	### Rationale
	The purpose of capDL is describing a snapshot of the capability
	distribution in a system running on the seL4 microkernel. For this
	purpose, we need to know which objects exist in the system and which
	capabilities they have access to. The second purpose of capDL is to
	serve as sufficiently detailed input to automated code generation
	tools. Therefore we need to include all information about capability
	arguments that such implementations will need. Some of this information
	will not be relevant for security analysis. For instance, for a
	security analysis it may be necessary to know which frames of physical
	memory an entity in the system can access via virtual memory, but it is
	not necessary to know under which virtual address each of these
	physical addresses is visible to the process. For a concrete
	implementation of a bootstrapping component on the other hand, this
	latter information is crucial.

	### The Model

	We refer to objects by name. This name could be of any type; for
	convenience we either use a plain string or a string with an index. We
	use the `Maybe` type of Haskell to express this.

	types ObjID = (String, Maybe Word)

	With this the capability state of a system is fully described by a map
	from `ObjID` to `Object`. Since not all objects and capabilities are
	supported by seL4 on all machine architectures, we also store which
	architecture the system is intended for.

	data Model = Model {
	arch :: Arch,
	objects :: Map ObjID Object
	}

	data Arch = IA32 \| ARM11

	Objects are described by the following data type. We are mainly
	interested in what capabilities an object contains. We also store
	information that is relevant for creating an object such as its type and
	its size when the size is configurable. This means in contrast to the
	security model, where we only talk about abstract entities, we give more
	detailed information in capDL.

	types CapMap = Map Word Cap

	data Object = Endpoint
	\| Notification
	\| TCB { slots :: CapMap, initArguments :: [Word] }
	\| CNode { slots :: CapMap, sizeBits :: Word }
	\| Untyped { maybeSizeBits :: Maybe Word }

	\| ASIDPool { slots :: CapMap }
	\| PT { slots :: CapMap }
	\| PD { slots :: CapMap }
	\| Frame { vmSizeBits :: Word }
	\| IOPorts { size :: Word }
	\| IOPT { slots :: CapMap, level :: Word }
	\| IODevice { slots :: CapMap }

	The first two objects, communication endpoints and notifications, do not
	store any capabilities and have a fixed size. Thread Control Blocks
	(TCB) contain a small number of capability registers, modelled by the
	field `slots`, a map from a machine word (the slot/register number) to
	the capability that is stored in that slot. Slots may be empty. CNode
	objects are the main capability storage object in seL4. They have
	configurable size. Untyped objects are conceptual containers for
	dynamically created objects. They cover a set of objects referred to by
	their `ObjID`. This set is called the covering set. In the
	implementation untyped objects must have a size, but in capDL
	specifications we often want to leave the size unspecified (as large as
	necessary).

	The next batch of objects in the data type above are architecture
	dependent. Most of these data structures and devices do not store actual
	capabilities in the kernel and hardware implementation. Instead they
	store pointers or mappings to other resources in the system. Since these
	resources are already represented as objects, we use capabilities to
	model these mappings and to express the access, for instance, a device
	may have to physical memory. In detail, the architecture dependent
	objects are as follows. ASID pools store which page directories (PD) can
	be activated by the machine. As mentioned, we represent this mapping as
	a capability in the model. Analogously, we model the mappings in virtual
	memory objects page directory (PD) and page table (PT). Physical memory
	frames (`Frame`) come in different sizes, depending on architecture, but
	do not contain further capabilities. IOMMU page tables (`IOPT`) come in
	multiple levels and again store mappings to frames or further page
	tables. Finally, hardware devices are represented by the object type
	`IODevice`. Again, we model the access hardware may have to resources in
	the system as capabilities. Specifically, IODevices may have a
	capability to a CNode for IRQ delivery, potentially multiple
	capabilities to physical memory frames for memory mapped device
	registers, and one capability for the root IOMMU space.

	To conclude the description of the capDL data model, it remains to
	define the data type of capabilities `Cap`. Almost all capabilities in
	seL4 refer to one specific object. Some may refer to a set of objects or
	implicitly to all objects of a given type. Many of the capabilities
	store explicit access rights. These are modelled as follows:

	data Rights = Read \| Write \| Grant \| GrantReply
	types CapRights = Set Right

	Again in contrast to the security model of seL4, we explicitly
	distinguish different types of capabilities in capDL and store slightly
	different kinds of additional information with each. As a side effect,
	we do not need an explicit representation of the create right. The
	create right is conferred by the possession of an untyped capability.

	data Cap = NullCap
	\| UntypedCap { capObj :: ObjID }
	\| EndpointCap { capObj :: ObjID, capBadge :: Word,
	capRights :: CapRights }
	\| NotificationCap { capObj :: ObjID, capBadge :: Word,
	capRights :: CapRights }
	\| ReplyCap { capObj :: ObjID }
	\| MasterReplyCap { capObj :: ObjID }
	\| CNodeCap { capObj :: ObjID, capGuard :: Word,
	capGuardSize :: Word }
	\| TCBCap { capObj :: ObjID }
	\| IRQControlCap
	\| IRQHandlerCap { capObj :: ObjID }
	\| FrameCap { capObj :: ObjID, capRights :: CapRights }
	\| PTCap { capObj :: ObjID }
	\| PDCap { capObj :: ObjID }
	\| ASIDControlCap
	\| ASIDPoolCap { capObj :: ObjID }
	\| IOPortsCap { capObjs :: Set Word }
	\| IOSpaceMasterCap
	\| IOSpaceCap { capObj :: ObjID }
	\| IOPTCap { capObj :: ObjID }

	In detail, the capabilities are as follows. We go through the list of
	capabilities and give a brief indication of the authority they convey.
	The `NullCap` is occasionally used to represent the absence of a
	capability. An untyped capability points to an untyped object and
	confers the right to issue create/retype and revoke/delete operations.
	Endpoint and notification capabilities point to their respective object
	types. They explicitly store which Read/Write/Grant access is conferred
	to the communications channel and they may carry one machine word of
	additional information, called the badge. CNode capabilities in addition
	to their CNode object reference carry information that influences the
	lookup of capabilities in the node they point to. This information
	consists of a guard in the sense of guarded page tables, the size of
	that guard, and finally the rights to the CNode object itself. A TCB cap
	gives authority over one TCB object with given access rights. The
	IRQControl capability gives authority to create specific IRQHandler
	capabilities. Each device may have a special CNode associated with it
	that may contain a notification which in turn is used to deliver
	interrupts to user level. IRQHandler caps in capDL point to these
	specific CNodes. It confers the authority to change which endpoint the
	interrupt is delivered to. Frame capabilities confer authority to map
	and unmap physical memory frames into and from a page directory or page
	table with the specified access rights. PT caps give authority to
	map/unmap page tables into/from page directories and PD caps give the
	authority to map/unmap page directories into ASID pools and to install
	them as virtual memory space of a process. The ASIDControlCap together
	with an Untyped cap confers authority to create new ASID pools. Only a
	limited, fixed number can be created in the system. ASIDPool caps give
	the authority to map/unmap page directories into/from the ASID pool.
	Mapping a frame into a page table for instance, needs the frame cap to
	specify which frame to map with which rights and the PT cap to specify
	in which page table. The IOPorts capability gives access to a set of
	IOPorts on the ia32 architecture. The IOSpaceMasterCap confers the
	authority to create IOSpace caps for specific devices. IOSpaceCaps point
	to IODevices and confer the authority to set the root IOPageTable for
	that device. IOPTCaps are the IOMMU analogue to PT and PD caps in normal
	virtual memory.

	## Semantics

	In this section, we define a mapping from the syntax of capDL to the
	data model of capDL. The mapping is defined by going over the relevant
	productions in the capDL grammar and describing the corresponding model.

	### Names and Ranges

	name ::= identifier

	Names are mapped to `ObjID`s in the model. A name without index maps to
	`(name, Nothing)`. Qualified names will be defined in the object
	declaration section.

	num ::= '[' number ']'

	This production maps to a single index and is used to either declare a
	set of objects, in which case the number is the number of objects, or to
	refer to a specific index. The term name\[x\] maps to the `ObjID`
	`(name, Just x)`.

	range ::= number '..' number \| '..' number \| number '..' \| number
	ranges ::= '[' ']' \| '[' range (',' range)* ']'
	name_ref ::= name ranges?

	Ranges stand for sets of `ObjID`s. For a set declared as `name[n]`, the
	following mappings apply:

	- `name[..b]` refers to `name[0]`, `name[1]`, .., `name[b]`

	- `name[a..]` refers to `name[a]`, `name[a+1]`, .., `name[n]`

	- `name[a..b]` refers to `name[a]`, `name[a+1]`, .., `name[b]`

	- `name[]` refers to `name[0]`, `name[1]`, .., `name[n]`

	A list of ranges `name[r1,r2,..r3]` refers to the union of the ranges
	`name[r1]`, `name[r2]`, .., `name[r3]`.

	### Module

	arch ::= 'arch' ('ia32' \| 'arm11')
	module ::= arch (obj_decls \| cap_decls)+

	A module maps to a full `Model` in the data model. Its `Arch` component
	is determined by `arch`, its mapping from `ObjID` to `Object` by the
	object and capability declarations described below.

	### Object Declarations

	obj_decls ::= 'objects' obj_decl*

	An object declaration section defines a set of objects. Each object name
	of typed objects should be declared only once. The covering set of
	untyped objects may be declared multiple times. The total covering set
	is the union of all covering sets mentioned for that object.

	obj_decl ::= qname '=' object

	An object declaration has a potentially qualified name and dimension on
	the left hand side and an object content declaration on the right hand
	side. A qualified name `name1/name2/name3[n]` implicitly declares the
	untyped objects `name1` and `name2`. It also declares that `name2` is
	covered by `name1` and `name3` covered by `name2`. Giving a dimension
	`[n]` means that n objects `(name3, Just 0)` to `(name3, Just (n-1))`
	are declared, each with the same content described on the right hand
	side of the equation.

	The right hand side is defined by the following syntax productions:

	object ::= object_type object_params? obj_decls?

	object_type ::= 'ep' \| 'notification' \| 'tcb' \| 'cnode' \| 'ut' \|
	'asid_pool' \| 'pt' \| 'pd' \| 'frame' \| 'io_ports' \|
	'io_device' \| 'io_pt'

	object_params ::= '(' object_param (',' object_param)* ')'

	object_param ::= obj_bit_size \| obj_vm_size \| io_pt_level \| obj_ports_size
	obj_bit_size ::= number 'bits'
	obj_vm_size ::= number ('k' \| 'M')
	io_pt_level ::= 'level' ':' ('1' \| '2' \| '3')
	obj_ports_size ::= number 'k' 'ports'

	obj_decls ::= '{' ((obj_decl \| name_ref) ','?)* '}'

	The object content is given by the type of the object mapping to its
	corresponding object type in the data model. Some of the object types in
	the model require a size parameter, given in bits (where n bits means a
	size of 2^n entries). Frames' sizes are specified directly as are the
	levels of IOMMU page tables. Untyped objects can be followed by a nested
	object declaration. Writing

	name1 = ut {
	name2/name3 [n] = object
	name2/name4 = object
	...
	}

	is equivalent to writing

	name1/name2/name3 [n] = object
	name1/name2/name4 = object
	...

	### Capability Declarations

	The capability content of objects is declared in its own section,
	separately from the list of objects itself.

	cap_decls = 'caps' (cap_name_decl \| cap_decl)*

	cap_name_decl ::= name '=' '(' name_ref ',' slot ')'
	slot ::= number \| symbolic_slot
	symbolic_slot ::= 'cspace' \| 'vspace'

	Next to capability content declarations, there are name declarations for
	capability slots. A capability slot is defined by the container object,
	referred to by a name reference (mapping to a single `ObjID`) and a slot
	inside the container specified by its slot number. The symbolic slot
	names `cspace`, `vspace` stand for slot numbers 0 and 1.

	A capability declaration starts with a set of container objects, each of
	which is declared to contain the capability mappings specified on the
	right hand side. Container objects may occur more than once in a
	specification. Their mappings are the union of all mappings for that
	container object.

	cap_decl ::= name_ref '{' (cap_mapping_or_ref ';'?)* '}'

	A cap mapping is specified by its slot and its capability and
	potentially an inline name declaration for the specified slot in the
	specified container.

	cap_mapping_or_ref ::= slot ':' cap_name? (cap_mapping \| cap_name_ref)

	cap_name ::= name '='
	cap_mapping ::= name_ref cap_params?
	cap_params ::= '(' cap_param (',' cap_param)* ')'

	cap_param ::= right+
	\| 'masked' ':' right+
	\| 'guard' ':' number
	\| 'guard_size' ':' number
	\| 'irq'
	\| 'badge' ':' number
	\| 'reply'
	\| 'master_reply'

	right ::= 'R' \| 'W' \| 'G'

	cap_name_ref ::= '<' name_ref '>' cap_params?

	The capability declaration is either a `cap_mapping` or `cap_name_ref`.
	In the latter case the mapping is a copy of the capability in the slot
	referred to by `name` (possibly `masked` with an access rights mask). In
	the former case, a cap is defined by the object it points to, together
	with optional parameters depending on the type of the object in the data
	model. For instance, an endpoint cap is specified if the `ObjID` given
	in the cap declaration refers to an endpoint object. If no parameters
	are mentioned, default parameters are substituted if possible. These
	defaults are: empty set of rights for access rights, full set of rights
	for rights masks, guard 0, guard size 0, and badge 0. The IRQControl cap
	is specified using the reserved `ObjID` `irq_control`, similarly
	ASIDControlCap is specified by `asid_control` and IOSpaceMasterCap by
	`io_space_master`.