This README file explains the source codes of our TEE API formal model.

======================================================
The Structure of the TEE API Formal Model (Directory)
======================================================


The directory 'src' of the top directory contains the source code for our formal model of TEE APIs.
Below is a brief description of each file separated into three categories.

- Formal model of the TEE API behavior

  - generic.maude.      	: Generic object with its behaviors.
  - transient.maude     	: Transient object with its behaviors. 
  - persistent.maude    	: Persistent object with its behaviors.
  - data-stream.maude   	: Data stream object with its behaviors.
  - enumerator.maude    	: Enumerator object with its behaviors.
  - cryptographic.maude 	: Cryptographic operation with its behavior.

- Formal model of the TEE infrastructure
  
  - objects.maude       	: Common storage objects (e.g., superclass object of transient and persistent objects).
  - handle.maude        	: Handle objects. 
  - constants.maude     	: Partial constants described in Global Platform spec.
  - data.maude          	: Functions handling data stream.
  - tee-data-type.maude 	: Data structures for TEE APIs described in Global Platform spec.
  - os.maude            	: Trusted OS object with its behavior and Device objects.
  - tee-client.maude    	: Trusted OS behaviors handling TEE Client API.
  - app.maude           	: Abstract program application object.
  - ree-app.maude       	: Rich application (RA) with its behaviors.
  - tee-app.maude      	  : Trusted application (TA) with its behaviors.
  - tee-kernel.maude    	: Trusted application kernel object.
  - tee-msg.maude       	: Message used for invoking TEE storage APIs.
  - tee-panic.maude    	  : TEE API panic.

- Programming language semantics using the K framework

  - tee-api.maude   : TEE APIs defined in Global Platform spec. Sec 5,6.
  - imp.maude       : Syntax and semantics of the language.
  - k-prelude.maude : K-framework foundation.
  - tee-imp.maude   : TEE API specific language semantics.

The main.maude file is the main maude file that includes all of the above-mentioned files.