Tock userspace applications must follow the Tock Binary Format (TBF). A TBF Object has four parts: a Header section, which encodes meta-data about the TBF Object, the actual Userspace Binary, an optional Footer section which encodes metadata about the TBF Object, and finally optional padding.
TBF Headers and Footers differ in how they are handled for TBF Object integrity. Integrity values (e.g., hashes) for a TBF Object are computed over the Header section and Userspace Binary but not the Footer Region or padding after footers. TBF Headers are covered by integrity, while TBF Footers are not covered by integrity.
Tock App Binary:
Start of app -> +-------------------+---
^ | TBF Header | ^
| +-------------------+ | Protected region
| | (Optional) | |
| | protected trailer | V
Covered by | +-------------------+---
integrity | | Userspace Binary |
| | |
| | |
V | |
+-------------------+
| Optional footers |
| (only if Program |
| header present) |
+-------------------+
| Optional padding |
+-------------------+
The header is interpreted by the kernel (and other tools, like tockloader) to understand important aspects of the app. In particular, the kernel must know where in the application binary is the entry point that it should start executing when running the app for the first time.
After the header the app is free to include whatever Userspace Binary it wants, and the format is completely up to the app. All support for relocations must be handled by the app itself, for example.
If the TBF Object has a Program Header in the Header section, the Userspace Binary can be followed by optional TBF Footers.
Finally, the TBF Object can be padded to a specific length. This is useful when a memory protection unit (MPU) restricts the length and offset of protection regions to powers of two. In such cases, padding allows a TBF Object to be padded to a power of two in size, so the next TBF Object is at a valid alignment.
Both TBF Footers and Headers follow the same TLV (type-length-value) format, to simplify parsing.
TBF Objects in Tock are stored sequentially. The start of TBF Object N+1 is immediately at the end of TBF Object N. Therefore, the TBF header specifies the length of the TBF Object so that the kernel can find the start of the next one.
If there is a gap between TBF Objects an "empty object" can be inserted to keep the structure intact.
Tock apps are typically stored in sorted order, from longest to shortest. This is to help match MPU rules about alignment.
A TBF Object can contain no code. A TBF Object can be marked as disabled to act as padding between other objects.
The TBF Header section contains all of a TBF Object's headers. All TBF Objects have a Base Header and the Base Header is always first. All headers are a multiple of 4 bytes long; the TBF Header section is multiple of 4 bytes long.
These are the Rust structures the kernel uses, defined in the
tock-tbf crate, to represent headers. Their in-flash
representations are described below.
struct TbfHeaderV2Base {
version: u16, // Version of the Tock Binary Format (currently 2)
header_size: u16, // Number of bytes in the TBF header section
total_size: u32, // Total padded size of the program image in bytes, including header
flags: u32, // Various flags associated with the application
checksum: u32, // XOR of all 4 byte words in the header, including existing optional structs
}After the Base Header come optional headers. Optional headers are structured as TLVs (type-length-values). Footers are encoded in the same way. Footers are also called headers for historical reasons: originally TBFs only had headers, and since footers follow the same format TBFs keep these types without changing their names.
// Identifiers for the optional header structs.
enum TbfHeaderTypes {
TbfHeaderMain = 1,
TbfHeaderWriteableFlashRegions = 2,
TbfHeaderPackageName = 3,
TbfHeaderPicOption1 = 4,
TbfHeaderFixedAddresses = 5,
TbfHeaderPermissions = 6,
TbfHeaderPersistent = 7,
TbfHeaderKernelVersion = 8,
TbfHeaderProgram = 9,
TbfFooterCredentials = 128,
}
// Type-length-value header to identify each struct.
struct TbfHeaderTlv {
tipe: TbfHeaderTypes, // 16 bit specifier of which struct follows
// When highest bit of the 16 bit specifier is set
// it indicates out-of-tree (private) TLV entry
length: u16, // Number of bytes of the following struct
}
// All apps must have a Main Header or a Program Header; it may
// have both. Without either, the "app" is considered padding and used
// to insert an empty linked-list element into the app flash space. If
// an app has both, it is the kernel's decision which to use. Older kernels
// use Main Headers, while newer (>= 2.1) kernels use Program Headers.
struct TbfHeaderMain {
base: TbfHeaderTlv,
init_fn_offset: u32, // The function to call to start the application
protected_trailer_size: u32, // The number of app-immutable bytes after the header
minimum_ram_size: u32, // How much RAM the application is requesting
}
// A Program Header specifies the end of the application binary within the
// TBF, such that the application binary can be followed by footers. It also
// has a version number, such that multiple versions of the same application
// can be installed.
pub struct TbfHeaderV2Program {
init_fn_offset: u32,
protected_trailer_size: u32,
minimum_ram_size: u32,
binary_end_offset: u32,
version: u32,
}
// Optional package name for the app.
struct TbfHeaderPackageName {
base: TbfHeaderTlv,
package_name: [u8], // UTF-8 string of the application name
}
// A defined flash region inside of the app's flash space.
struct TbfHeaderWriteableFlashRegion {
writeable_flash_region_offset: u32,
writeable_flash_region_size: u32,
}
// One or more specially identified flash regions the app intends to write.
struct TbfHeaderWriteableFlashRegions {
base: TbfHeaderTlv,
writeable_flash_regions: [TbfHeaderWriteableFlashRegion],
}
// Fixed and required addresses for process RAM and/or process flash.
struct TbfHeaderV2FixedAddresses {
base: TbfHeaderTlv,
start_process_ram: u32,
start_process_flash: u32,
}
struct TbfHeaderDriverPermission {
driver_number: u32,
offset: u32,
allowed_commands: u64,
}
// A list of permissions for this app
struct TbfHeaderV2Permissions {
base: TbfHeaderTlv,
length: u16,
perms: [TbfHeaderDriverPermission],
}
// A list of storage permissions for accessing persistent storage
struct TbfHeaderV2StoragePermissions {
base: TbfHeaderTlv,
write_id: u32,
read_length: u16,
read_ids: [u32],
modify_length: u16,
modify_ids: [u32],
}
// Kernel Version
struct TbfHeaderV2KernelVersion {
base: TbfHeaderTlv,
major: u16,
minor: u16
}
// Types of credentials footers
pub enum TbfFooterV2CredentialsType {
Reserved = 0,
Rsa3072Key = 1,
Rsa4096Key = 2,
SHA256 = 3,
SHA384 = 4,
SHA512 = 5,
}
// Credentials footer. The length field of the TLV determines
// the size of the data slice.
pub struct TbfFooterV2Credentials {
format: TbfFooterV2CredentialsType,
data: &'static [u8],
}The TBF Header section contains a Base Header, followed by a sequence of type-length-value encoded elements. All fields in both the base header and TLV elements are little-endian. The base header is 16 bytes, and has 5 fields:
0 2 4 6 8
+-------------+-------------+---------------------------+
| Version | Header Size | Total Size |
+-------------+-------------+---------------------------+
| Flags | Checksum |
+---------------------------+---------------------------+
-
Versiona 16-bit unsigned integer specifying the TBF header version. Always2. -
Header Sizea 16-bit unsigned integer specifying the length of the entire TBF header in bytes (including the base header and all TLV elements). -
Total Sizea 32-bit unsigned integer specifying the total size of the TBF in bytes (including the header). -
Flagsspecifies properties of the process.3 2 1 0 1 0 9 8 7 6 5 4 3 2 1 0 9 8 7 6 5 4 3 2 1 0 9 8 7 6 5 4 3 2 1 0 +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Reserved |S|E| +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- Bit 0 marks the process enabled. A
1indicates the process is enabled. Disabled processes will not be launched at startup. - Bit 1 marks the process as sticky. A
1indicates the process is sticky. Sticky processes require additional confirmation to be erased. For example,tockloaderrequires the--forceflag erase them. This is useful for services running as processes that should always be available. - Bits 2-31 are reserved and should be set to 0.
- Bit 0 marks the process enabled. A
-
Checksumthe result of XORing each 4-byte word in the header, excluding the word containing the checksum field itself.
The header is followed immediately by a sequence of TLV elements. TLV elements are aligned to 4 bytes. If a TLV element size is not 4-byte aligned, it will be padded with up to 3 bytes. Each element begins with a 16-bit type and 16-bit length followed by the element data:
0 2 4
+-------------+-------------+-----...---+
| Type | Length | Data |
+-------------+-------------+-----...---+
Typeis a 16-bit unsigned integer specifying the element type.Lengthis a 16-bit unsigned integer specifying the size of the data field in bytes.Datais the element specific data. The format for thedatafield is determined by itstype.
TBF may contain arbitrary element types. To avoid type ID collisions between elements defined by the Tock project and elements defined out-of-tree, the ID space is partitioned into two segments. Type IDs defined by the Tock project will have their high bit (bit 15) unset, and type IDs defined out-of-tree should have their high bit set.
The Main element has three 32-bit fields:
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (1) | Length (12) | init_offset |
+-------------+-------------+---------------------------+
| protected_trailer_size | min_ram_size |
+---------------------------+---------------------------+
init_offsetthe offset in bytes from the beginning of binary payload (i.e. the actual application binary) that contains the first instruction to execute (typically the_startsymbol).protected_trailer_sizethe size of the protected region after the TBF headers. Processes do not have write access to the protected region. TBF headers are contained in the protected region, but are not counted towardsprotected_trailer_size. The protected region thus starts at the first byte of the TBF base header, and isheader_size + protected_trailer_sizebytes in size.minimum_ram_sizethe minimum amount of memory, in bytes, the process needs.
If the Main TLV header is not present, these values all default to 0.
The Main Header and Program Header have overlapping functionality. If a TBF Object has both, the kernel decides which to use. Tock is transitioning to having the Program Header as the standard one to use, but older kernels (2.0 and earlier) do not recognize it and use the Main Header.
Writeable flash regions indicate portions of the binary that the process
intends to mutate in flash.
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (2) | Length (8) | offset |
+-------------+-------------+-------------+-------------+
| size |
+---------------------------+
offsetthe offset from the beginning of the binary of the writeable region.sizethe size of the writeable region.
The Package name specifies a unique name for the binary. Its only field is
an UTF-8 encoded package name.
0 2 4
+-------------+-------------+----------...-+
| Type (3) | Length | package_name |
+-------------+-------------+----------...-+
package_nameis an UTF-8 encoded package name
Fixed Addresses allows processes to specify specific addresses they need for
flash and RAM. Tock supports position-independent apps, but not all apps are
position-independent. This allows the kernel (and other tools) to avoid loading
a non-position-independent binary at an incorrect location.
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (5) | Length (8) | ram_address |
+-------------+-------------+-------------+-------------+
| flash_address |
+---------------------------+
ram_addressthe address in memory the process's memory address must start at. If a fixed address is not required this should be set to0xFFFFFFFF.flash_addressthe address in flash that the process binary (not the header) must be located at. This would match the value provided for flash to the linker. If a fixed address is not required this should be set to0xFFFFFFFF.
The Permissions section allows an app to specify driver permissions that it is
allowed to use. All driver syscalls that an app will use must be listed. The
list should not include drivers that are not being used by the app.
The data is stored in the optional TbfHeaderV2Permissions field. This includes
an array of all the perms.
0 2 4 6
+-------------+-------------+-------------+---------...--+
| Type (6) | Length | # perms | perms |
+-------------+-------------+-------------+---------...--+
The perms array is made up of a number of elements of
TbfHeaderDriverPermission. The first 16-bit field in the TLV is the number of
driver permission structures included in the perms array. The elements in
TbfHeaderDriverPermission are described below:
Driver Permission Structure:
0 2 4 6 8
+-------------+-------------+---------------------------+
| driver_number | offset |
+-------------+-------------+-------------+-------------+
| allowed_commands |
+-------------------------------------------------------+
driver_numberis the number of the driver that is allowed. This for example could be0x00000to indicate that theAlarmsyscalls are allowed.allowed_commandsis a bit mask of the allowed commands. For example a value of0b0001indicates that only command 0 is allowed.0b0111would indicate that commands 2, 1 and 0 are all allowed. Note that this assumesoffsetis 0, for more details onoffsetsee below.- The
offsetfield inTbfHeaderDriverPermissionindicates the offset of theallowed_commandsbitmask. All of the examples described in the paragraph above assume anoffsetof 0. Theoffsetfield indicates the start of theallowed_commandsbitmask. Theoffsetis multiple by 64 (the size of theallowed_commandsbitmask). For example anoffsetof 1 and aallowed_commandsvalue of0b0001indicates that command 64 is allowed.
Subscribe and allow commands are always allowed as long as the specific
driver_number has been specified. If a driver_number has not been specified
for the capsule driver then allow and subscribe will be blocked.
Multiple TbfHeaderDriverPermission with the same driver_numer can be
included, so long as no offset is repeated for a single driver. When
multiple offsets and allowed_commandss are used they are ORed together,
so that they all apply.
The Storage Permissions section is used to identify what access the app has to
persistent storage.
The data is stored in the TbfHeaderV2StoragePermissions field, which includes
a write_id, a number of read_ids, and a number of modify_ids.
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (7) | Length | write_id |
+-------------+-------------+---------------------------+
| # Read IDs | read_ids (4 bytes each) |
+-------------+------------------------------------...--+
| # Modify IDs| modify_ids (4 bytes each) |
+--------------------------------------------------...--+
write_idindicates the id that all new persistent data is written with. All new data created will be stored with permissions from thewrite_idfield. For existing data see themodify_idssection below.write_iddoes not need to be unique, that is multiple apps can have the same id. Awrite_idof0x00indicates that the app can not perform write operations.read_idslist all of the ids that this app has permission to read. Theread_lengthspecifies the length of theread_idsin elements (not bytes).read_lengthcan be0indicating that there are noread_ids.modify_idslist all of the ids that this app has permission to modify or remove.modify_idsare different fromwrite_idin thatwrite_idapplies to new data whilemodify_idsallows modification of existing data. Themodify_lengthspecifies the length of themodify_idsin elements (not bytes).modify_lengthcan be0indicating that there are nomodify_idsand the app cannot modify existing stored data (even data that it itself wrote).
For example, consider an app that has a write_id of 1, read_ids of 2, 3
and modify_ids of 3, 4. If the app was to write new data, it would be stored
with id 1. The app is able to read data stored with id 2 or 3, note that
it cannot read the data that it writes. The app is also able to overwrite
existing data that was stored with id 3 or 4.
An example of when modify_ids would be useful is on a system where each app
logs errors in its own write_region. An error-reporting app reports these errors
over the network, and once the reported errors are acked erases them from the
log. In this case, modify_ids allow an app to erase multiple different
regions.
The compatibility header is designed to prevent the kernel
from running applications that are not compatible with it.
It defines the following two items:
Kernel majororVis the kernel major number (for Tock 2.0, it is 2)Kernel minororvis the kernel minor number (for Tock 2.0, it is 0)
Apps defining this header are compatible with kernel version ^V.v (>= V.v and < (V+1).0)
The kernel version header refers only to the ABI and API exposed by the kernel itself, it does not cover API changes within drivers.
A kernel major and minor version guarantees the ABI for exchanging data between kernel and userspace and the the system call numbers.
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (8) | Length (4) | Kernel major| Kernel minor|
+-------------+-------------+---------------------------+
A Program Header is an extended form of the Main Header. It adds two
fields, binary_end_offset and version. The binary_end_offset field
allows the kernel to identify where in the TBF object the application
binary ends. The gap between the end of the application binary and
the end of the TBF object can contain footers.
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (9) | Length (20) | init_offset |
+-------------+-------------+---------------------------+
| protected_trailer_size | min_ram_size |
+---------------------------+---------------------------+
| binary_end_offset | version |
+---------------------------+---------------------------+
init_offsetthe offset in bytes from the beginning of binary payload (i.e. the actual application binary) that contains the first instruction to execute (typically the_startsymbol).protected_trailer_sizethe size of the protected region after the TBF headers. Processes do not have write access to the protected region. TBF headers are contained in the protected region, but are not counted towardsprotected_trailer_size. The protected region thus starts at the first byte of the TBF base header, and isheader_size + protected_trailer_sizebytes in size.minimum_ram_sizethe minimum amount of memory, in bytes, the process needs.binary_end_offsetspecifies the offset from the beginning of the TBF Object at which the Userspace Binary ends and optional footers begin.versionspecifies a version number for the application implemented by the Userspace Binary. This allows a kernel to distinguish different versions of a given application.
If a Program header is not present, binary_end_offset can be
considered to be total_size of the Base Header and version is 0.
The Main Header and Program Header have overlapping functionality. If a TBF Object has both, the kernel decides which to use. Tock is transitioning to having the Program Header as the standard one to use, but older kernels (2.0 and earlier) do not recognize it and use the Main Header.
A Credentials Footer contains cryptographic credentials for the integrity and possibly identity of a Userspace Binary. A Credentials Footer has the following format:
0 2 4 6 8
+-------------+-------------+---------------------------+
| Type (128) | Length (4+n)| format |
+-------------+-------------+---------------------------+
| data...
+---------------------------+---------------------------+
The length of the data field is defined by the Length field. If
the data field is n bytes long, the Length field is 4+n. The
format field defines the format of the data field:
pub enum TbfFooterV2CredentialsType {
Reserved = 0,
Rsa3072Key = 1,
Rsa4096Key = 2,
SHA256 = 3,
SHA384 = 4,
SHA512 = 5,
}TRD-appid provides further details on TBF Credentials Footers, their format, and processing.
The process code itself has no particular format. It will reside in flash, but the specific address is determined by the platform. Code in the binary should be able to execute successfully at any address, e.g. using position independent code.