This file provides the basic interface of the CSL language constructs for use within the H2020 TeamPlay project. Inspired by teamplay_reel.h. More...

Data Structures
struct	__csl_nonground_int
	A type for representing variables in CSL assertions for which a value is not known. More...

Macros
#define	__csl_component_application(x) void dummy_csl_fn_ ## x()
	A declaration-level CSL annotation that defines the name of the application for the component file. More...

#define	__csl_component(x) void dummy_csl_fn_ ## x()
	A declaration-level CSL annotation for the identification of functions as components. More...

Functions
void	__csl_security_set_secret (unsigned long long *var)
	__csl_security_set_secret assigns a flag to a given TeamPlay variable stating its secret status. More...

void	__csl_time_worst (unsigned long long *var)
	__csl_time_worst assigns WCET (Worst-Case Execution Time) values to a given TeamPlay variable. More...

void	__csl_average_time (unsigned long long *var)
	__csl_average_time assigns WCET (Average-Case Execution Time) values to a given TeamPlay variable. More...

void	__csl_energy (unsigned long long *var)
	__csl_energy assigns Average-Case Energy Usage (ACEU) values to a given TeamPlay variable. More...

void	__csl_security_crypto (unsigned long long *var)
	__csl_security_crypto assigns cryptographic strength values to a given TeamPlay variable. More...

void	__csl_security_sca_time_worst (unsigned long long *var)
	__csl_security_sca_time_worst assigns WCDT (Worst-Case Discernible Time) values to a given TeamPlay variable. More...

void	__csl_security_sca_time_average (unsigned long long *var)
	__csl_security_sca_time_average assigns ACDT (Average-Case Discernible Time) values to a given TeamPlay variable. More...

void	__csl_security_sca_time_ratio (unsigned long long *var)
	__csl_security_sca_time_ratio assigns IIRT (Indiscernible Information Ratio for Time) values to a given TeamPlay variable. More...

void	__csl_security_sca_energy_worst (unsigned long long *var)
	__csl_security_sca_energy_worst assigns WCDE (Worst-Case Discernible Energy) values to a given TeamPlay variable. More...

void	__csl_security_sca_energy_average (unsigned long long *var)
	__csl_security_sca_energy_average assigns ACDE (Average-Case Discernible Energy) values to a given TeamPlay variable. More...

void	__csl_security_sca_energy_ratio (unsigned long long *var)
	__csl_security_sca_energy_ratio assigns IIRE (Indiscernible Information Ratio for Energy) values to a given TeamPlay variable. More...

void	__csl_security_sca_power_worst (unsigned long long *var)
	__csl_security_sca_power_worst assigns WCDP (Worst-Case Discernible Power) values to a given TeamPlay variable. More...

void	__csl_security_sca_power_average (unsigned long long *var)
	__csl_security_sca_power_average assigns ACDP (Average-Case Discernible Power) values to a given TeamPlay variable. More...

void	__csl_security_sca_power_ratio (unsigned long long *var)
	__csl_security_sca_energy_ratio assigns IIRP (Indiscernible Information Ratio for Power) values to a given TeamPlay variable. More...

void	__csl_assert (_Bool expr)
	__csl_assert provides C-level contracts in order to enable expression of (non-functional) properties within the program; assertion annotations are used in the generation of Idris proofs of the assertion. More...

void	__csl_assert_nonground (struct __csl_nonground_int *ngvar, _Bool expr)
	A non-ground assertion; to be defined. More...

void	__csl_component_deadline (unsigned long long deadline)
	CSL Component annotation used to define the deadline of either an application or a specific (version of a) component. More...

void	__csl_component_period (unsigned long long period)
	CSL Component annotation used to define the period of either an application or a specific (version of a) component. More...

void	__csl_component_energy_available (unsigned long long energy)
	CSL Component annotation used to define the energy available for an application. More...

void	__csl_component_type_alias (char alias[], char type[], void *dValue)
	CSL Component annotation used to define a type alias of a standard C type, along with a default value for that type, to be used in input/output annotations. More...

void	__csl_component_input (char label[], unsigned long long consume, char alias[])
	CSL Component annotation used to define an input channel of a component. More...

void	__csl_component_output (char label[], unsigned long long produce, char alias[], char edges[])
	CSL Component annotation used to define an output channel of a component. More...

void	__csl_component_version (char label[])
	CSL Component annotation used to indicate that the annotated function is a version of a component. More...

void	__csl_component_security (unsigned long long secLevel)
	CSL Component annotation used to indicate that a component version has a given security level. More...

void	__csl_component_arch (char arch_label[])
	CSL Component annotation used to indicate that a component version is designed for a given architecture. More...

void	__csl_component_wcet (unsigned long long wcet)
	CSL Component annotation used to indicate that a component version has a given worst-case execution time. More...

void	__csl_component_wcec (unsigned long long wcec)
	CSL Component annotation used to indicate that a component version has a given worst-case energy consumption value. More...

Detailed Description

This file provides the basic interface of the CSL language constructs for use within the H2020 TeamPlay project. Inspired by teamplay_reel.h.

Author: Adam D. Barwell adb23.nosp@m.@st-.nosp@m.andre.nosp@m.ws.a.nosp@m.c.uk

Definition in file csl.h.

Macro Definition Documentation

◆ __csl_component

#define __csl_component ( x ) void dummy_csl_fn_ ## x()

A declaration-level CSL annotation for the identification of functions as components.

Parameters

x	The name of the component.

The body of __csl_component may contain nine kinds of annotation:

__csl_component_input
__csl_component_output
__csl_component_deadline
__csl_component_period
__csl_component_version
__csl_component_security
__csl_component_arch
__csl_component_wcet
__csl_component_wcec

Multiple __csl_component_input and __csl_component_output annotations are permitted, but at least one of either is required. For all other annotation kinds, a maximum of one annotation is permitted.

In order to ensure that the component is callable from the scheduler, it is required that the annotated function and the parameter of the component annotation are the same. Where a __csl_component_version occurs, the name of the annotated function is required to be the component name extended with the version name. These requirements could be relaxed in future.

Where two component annotations have the same arguments (i.e. name), but also have a version annotation, those annotations will be rewritten as a single component entry with the original annotations represented by (potentially empty) version blocks. Additional version-specific annotations, i.e. those pertaining to security, target archi- tecture, or worst-case analyses, are thus added to the relevant version block. Only one of each version-specific annotations may occur within a compo- nent annotation, with the exception of the target architecture annotation. A component annotation that includes a version annotation may omit input, output, deadline, and period annotations on the assumption that these are defined in another component annotation for a different version of the same component. Two component annotations with the same name but without version annotations are deemed invalid.

Definition at line 404 of file csl.h.

◆ __csl_component_application

#define __csl_component_application ( x ) void dummy_csl_fn_ ## x()

A declaration-level CSL annotation that defines the name of the application for the component file.

The body of __csl_component_application may contain four kinds of annotation:

__csl_component_deadline
__csl_component_period
__csl_component_energy_available
__csl_component_type_alias

Multiple __csl_component_type_alias annotations may occur within a __csl_component_application, otherwise only one of each annotation kind may occur. It is assumed that there will be only one __csl_component_application annotation per program.

__csl_component_application is rewritten as an Application block using the given name as its identifier and, with two exceptions, the CSL component annotations occurring in its body as its fields. The components field is generated from __csl_component annotations outwith the body of the __csl_component_application annotation. The edges field is generated from __csl_component_input and __csl_component_output annotations in __csl_component annotations.

Definition at line 364 of file csl.h.

Function Documentation

◆ __csl_assert()

void __csl_assert ( _Bool expr )

__csl_assert provides C-level contracts in order to enable expression of (non-functional) properties within the program; assertion annotations are used in the generation of Idris proofs of the assertion.

Parameters

expr	A Boolean C expression that shall be asserted.

This annotation corresponds to the __reel_assert REEL annotation.

__csl_assert annotations are replaced with __reel_assert annotations. Note that, unlike REEL assertions, the CSL assertion langauge does not, in principle, require that assertions are in integer-linear form. Assertions that are integer-linear inequations and use only TeamPlay variables will not be changed. Conversely, assertions that use standard C variables or are not integer-linear inequations will be transformed in a manner that is still undefined; examples are welcome to aid definition of this transformation. Until this transformation is defined, assume that such CSL assertions are removed during the CSL to REEL transformation stage.

Note that, at present, the assertion language is quite restrictive. This can be extended according to need.

An assertion is a boolean expression in the form LHS <op> RHS, where LHS and RHS are terms as specified below, and <op> is a comparison operator from the set { <, <=, ==, !=, >=, > }.

LHS and RHS are arithmetic expressions,

e ::= n | x | e + e | e * e

comprising literal (constant) values, n; variables, x; and addition and multiplication operators, (+) and (*). All variables must be in scope and bound to some value at the location of the assertion. The values of variables at the location of the assertion will be used to generate proofs of the assertion.

For practical reasons, we presently assume that literal values are natural numbers (expressed as integers in C). Again, this assumption may be relaxed according to need.

◆ __csl_assert_nonground()

void __csl_assert_nonground	(	struct __csl_nonground_int *	ngvar,
		_Bool	expr
	)

A non-ground assertion; to be defined.

Parameters

ngvar	the free variable whose value/range of values is to be determined
expr	A Boolean C expression that shall be asserted.

Only the value of ngvar is unknown; all other variables in expr must be in scope and assigned to some value at the location of the assertion.

◆ __csl_average_time()

void __csl_average_time ( unsigned long long * var )

__csl_average_time assigns WCET (Average-Case Execution Time) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a WCET value shall be assigned.

This annotation corresponds to the __reel_average_time and __reel_average_time_manual REEL annotations. In the presence of an entry in the expert file for var and a given architecture, this annotation is rewritten into a __reel_average_time_manual annotation using the information in the expert file entry. Otherwise, i.e. when no entry exists for that variable and/ or for that given architecture, the annotation is rewritten into a __reel_average_time annotation, preserving both the parameter and the location of the annotation.

Since __reel_average_time requires that var is a scalar variable, we assume that the variable passed to __csl_average_time is a scalar variable; in the future, we intend for the transformation to fail when this requirement is not met.

The WCET value assigned to TeamPlay variable var refers to the Average-Case Execution Time of the immedately next non-CSL C statement.

The values stored in var represent processor clock cycles.

◆ __csl_component_arch()

void __csl_component_arch ( char arch_label[] )

CSL Component annotation used to indicate that a component version is designed for a given architecture.

◆ __csl_component_deadline()

void __csl_component_deadline ( unsigned long long deadline )

CSL Component annotation used to define the deadline of either an application or a specific (version of a) component.

◆ __csl_component_energy_available()

void __csl_component_energy_available ( unsigned long long energy )

CSL Component annotation used to define the energy available for an application.

◆ __csl_component_input()

void __csl_component_input	(	char	label[],
		unsigned long long	consume,
		char	alias[]
	)

CSL Component annotation used to define an input channel of a component.

Parameters

label	An identifier of the input channel.
consume	The number of tokens that is consumed upon reading from the channel.
alias	The type of the tokens expected along the channel.

◆ __csl_component_output()

void __csl_component_output	(	char	label[],
		unsigned long long	produce,
		char	alias[],
		char	edges[]
	)

CSL Component annotation used to define an output channel of a component.

Parameters

label	An identifier of the output channel.
produce	The number of tokens that is produced upon writing to the channel.
alias	The type of the tokens expected along the channel.
edges	A string representing the possible destination(s) for tokens along the channel.

◆ __csl_component_period()

void __csl_component_period ( unsigned long long period )

CSL Component annotation used to define the period of either an application or a specific (version of a) component.

◆ __csl_component_security()

void __csl_component_security ( unsigned long long secLevel )

CSL Component annotation used to indicate that a component version has a given security level.

◆ __csl_component_type_alias()

void __csl_component_type_alias	(	char	alias[],
		char	type[],
		void *	dValue
	)

CSL Component annotation used to define a type alias of a standard C type, along with a default value for that type, to be used in input/output annotations.

◆ __csl_component_version()

void __csl_component_version ( char label[] )

CSL Component annotation used to indicate that the annotated function is a version of a component.

◆ __csl_component_wcec()

void __csl_component_wcec ( unsigned long long wcec )

CSL Component annotation used to indicate that a component version has a given worst-case energy consumption value.

◆ __csl_component_wcet()

void __csl_component_wcet ( unsigned long long wcet )

CSL Component annotation used to indicate that a component version has a given worst-case execution time.

◆ __csl_energy()

void __csl_energy ( unsigned long long * var )

__csl_energy assigns Average-Case Energy Usage (ACEU) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which an ACEU value shall be assigned.

This annotation is analogous to the __csl_time_worst annotation above.

The __csl_energy annotation corresponds to the __reel_energy and __reel_energy_manual REEL annotations. In the presence of an entry in the expert file for var and a given architecture, this annotation is rewritten into a __reel_energy_manual annotation using the information in the expert file entry. Otherwise, i.e. when no entry exists for that variable and/ or for that given architecture, the annotation is rewritten into a __reel_energy annotation, preserving both the parameter and the location of the annotation.

Since __reel_energy requires that var is a scalar variable, we assume that the variable passed to __csl_energy is a scalar variable; in the future, we intend for the transformation to fail when this requirement is not met.

All ACEU values handled by __reel_energy are represented in Femtojoules. The ACEU value assigned to TeamPlay variable var refers to the Average-Case Energy Usage of the immedately next non-CSL C statement.

◆ __csl_security_crypto()

void __csl_security_crypto ( unsigned long long * var )

__csl_security_crypto assigns cryptographic strength values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a cryptographic strength value shall be assigned.

The cryptographic strength value assigned to TeamPlay variable var refers to the the strength of the immediately next non-CSL C cryptographic algorithm.

Author: Yoann Marquer

◆ __csl_security_sca_energy_average()

void __csl_security_sca_energy_average ( unsigned long long * var )

__csl_security_sca_energy_average assigns ACDE (Average-Case Discernible Energy) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a ACDE value shall be assigned.

The ACDE value assigned to TeamPlay variable var refers to the Average-Case Discernible Energy of the immediately next non-CSL C statement.

It reflects how easy it is for the attacker to find a point of interest from side-channel observations on consumed energy, expressed in femtojoules.

Author: Yoann Marquer

◆ __csl_security_sca_energy_ratio()

void __csl_security_sca_energy_ratio ( unsigned long long * var )

__csl_security_sca_energy_ratio assigns IIRE (Indiscernible Information Ratio for Energy) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a IIRE value shall be assigned.

The IIRE value assigned to TeamPlay variable var refers to the Indiscernible Information Ratio for Energy of the immediately next non-CSL C statement.

It reflects the reduction of the exploration space of the secret from the attacker point of view after observations done on consumed energy. It is a ratio between 0 and 1, 0% meaning no security and 100% meaning full security. It has been turned into an integer in range [0, 65535] for compatibility with WCC, hence the value should be divided by 65535 and turned into a float to recover its original meaning.

Author: Yoann Marquer

◆ __csl_security_sca_energy_worst()

void __csl_security_sca_energy_worst ( unsigned long long * var )

__csl_security_sca_energy_worst assigns WCDE (Worst-Case Discernible Energy) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a WCDE value shall be assigned.

The WCDE value assigned to TeamPlay variable var refers to the Worst-Case Discernible Energy of the immediately next non-CSL C statement.

It reflects the worst distance possible between secret-dependent side-channel observations done by the attacker on consumed energy, expressed in femtojoules.

Author: Yoann Marquer

◆ __csl_security_sca_power_average()

void __csl_security_sca_power_average ( unsigned long long * var )

__csl_security_sca_power_average assigns ACDP (Average-Case Discernible Power) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a ACDP value shall be assigned.

The ACDP value assigned to TeamPlay variable var refers to the Average-Case Power Distinguishability of the immediately next non-CSL C statement.

It reflects how easy it is for the attacker to find a point of interest from side-channel observations on power traces. This annotation is not supported by WCC yet, because of lack of a power analysis tool.

Author: Yoann Marquer

◆ __csl_security_sca_power_ratio()

void __csl_security_sca_power_ratio ( unsigned long long * var )

__csl_security_sca_energy_ratio assigns IIRP (Indiscernible Information Ratio for Power) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a IIRP value shall be assigned.

The IIRP value assigned to TeamPlay variable var refers to the Indiscernible Information Ratio for Power of the immediately next non-CSL C statement.

It reflects the reduction of the exploration space of the secret from the attacker point of view after observations done on power traces. It is a ratio between 0 and 1, 0% meaning no security and 100% meaning full security. This annotation is not supported by WCC yet, because of lack of a power analysis tool.

Author: Yoann Marquer

◆ __csl_security_sca_power_worst()

void __csl_security_sca_power_worst ( unsigned long long * var )

__csl_security_sca_power_worst assigns WCDP (Worst-Case Discernible Power) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a WCDP value shall be assigned.

The WCDP value assigned to TeamPlay variable var refers to the Worst-Case Power Distinguishability of the immediately next non-CSL C statement.

It reflects the worst distance possible between secret-dependent side-channel observations done by the attacker on power traces. This annotation is not supported by WCC yet, because of lack of a power analysis tool.

Author: Yoann Marquer

◆ __csl_security_sca_time_average()

void __csl_security_sca_time_average ( unsigned long long * var )

__csl_security_sca_time_average assigns ACDT (Average-Case Discernible Time) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a ACDT value shall be assigned.

The ACDT value assigned to TeamPlay variable var refers to the Average-Case Discernible Time of the immediately next non-CSL C statement.

It reflects how easy it is for the attacker to find a point of interest from side-channel observations on execution time, expressed in clock cycles.

Author: Yoann Marquer

◆ __csl_security_sca_time_ratio()

void __csl_security_sca_time_ratio ( unsigned long long * var )

__csl_security_sca_time_ratio assigns IIRT (Indiscernible Information Ratio for Time) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a IIRT value shall be assigned.

The IIRT value assigned to TeamPlay variable var refers to the Indiscernible Information Ratio for Time of the immediately next non-CSL C statement.

It reflects the reduction of the exploration space of the secret from the attacker point of view after observations done on execution time. It is a ratio between 0 and 1, 0% meaning no security and 100% meaning full security. It has been turned into an integer in range [0, 65535] for compatibility with WCC, hence the value should be divided by 65535 and turned into a float to recover its original meaning.

Author: Yoann Marquer

◆ __csl_security_sca_time_worst()

void __csl_security_sca_time_worst ( unsigned long long * var )

__csl_security_sca_time_worst assigns WCDT (Worst-Case Discernible Time) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a WCTD value shall be assigned.

The WCDT value assigned to TeamPlay variable var refers to the Worst-Case Discernible Time of the immediately next non-CSL C statement.

It reflects the worst distance possible between secret-dependent side-channel observations done by the attacker on execution time, expressed in clock cycles.

Author: Yoann Marquer

◆ __csl_security_set_secret()

void __csl_security_set_secret ( unsigned long long * var )

__csl_security_set_secret assigns a flag to a given TeamPlay variable stating its secret status.

Parameters

var	A pointer to a TeamPlay variable.

This annotation indicates to Inria security tools, especially the taint analysis, that in the immediately next non-CSL C statement the variable will be treated as a secret variable.

By default, the variables without this annotation will be treated as public variables.

Author: Yoann Marquer

◆ __csl_time_worst()

void __csl_time_worst ( unsigned long long * var )

__csl_time_worst assigns WCET (Worst-Case Execution Time) values to a given TeamPlay variable.

Parameters

var	A pointer to a TeamPlay variable to which a WCET value shall be assigned.

This annotation corresponds to the __reel_worst_time and __reel_worst_time_manual REEL annotations. In the presence of an entry in the expert file for var and a given architecture, this annotation is rewritten into a __reel_worst_time_manual annotation using the information in the expert file entry. Otherwise, i.e. when no entry exists for that variable and/ or for that given architecture, the annotation is rewritten into a __reel_worst_time annotation, preserving both the parameter and the location of the annotation.

Since __reel_worst_time requires that var is a scalar variable, we assume that the variable passed to __csl_time_worst is a scalar variable; in the future, we intend for the transformation to fail when this requirement is not met.

The WCET value assigned to TeamPlay variable var refers to the Worst-Case Execution Time of the immedately next non-CSL C statement.

The values stored in var represent processor clock cycles.

Data Structures

Macros

Functions

Detailed Description

Macro Definition Documentation

◆ __csl_component

◆ __csl_component_application

Function Documentation

◆ __csl_assert()

◆ __csl_assert_nonground()

◆ __csl_average_time()

◆ __csl_component_arch()

◆ __csl_component_deadline()

◆ __csl_component_energy_available()

◆ __csl_component_input()

◆ __csl_component_output()

◆ __csl_component_period()

◆ __csl_component_security()

◆ __csl_component_type_alias()

◆ __csl_component_version()

◆ __csl_component_wcec()

◆ __csl_component_wcet()

◆ __csl_energy()

◆ __csl_security_crypto()

◆ __csl_security_sca_energy_average()

◆ __csl_security_sca_energy_ratio()

◆ __csl_security_sca_energy_worst()

◆ __csl_security_sca_power_average()

◆ __csl_security_sca_power_ratio()

◆ __csl_security_sca_power_worst()

◆ __csl_security_sca_time_average()

◆ __csl_security_sca_time_ratio()

◆ __csl_security_sca_time_worst()

◆ __csl_security_set_secret()

◆ __csl_time_worst()