Lisex Security Model (LSM 0.0)

This specification is an abstract model of a file system compatible with Linux (or other UNIX flavors). It takes the form of a state machine. The specification is written in Coq and documented with coqdoc. The specification has been scarcely commented; those readers who want a more detailed explanation may consult [Cristiá, or this summary]. This file LSM00.tar.gz contains the source code of the specification, ready to be compiled with Coq 7.3; also you can download it from the Contribution section of the Coq site.

The file system state is defined as a record storing all the elements relevant to the security problem (files, directories, access classes, ACLs, open files, and so on). Also, a system initial state is given.

Then, every file system call is represented by an operation. Each operation is constructively defined through an inductive type in terms of its pre and postconditions. There are two kinds of operations:

• Those which require data about the system state but cannot produce a state change

	aclstat
	oscstat
	read
	readdir
	sscstat
	stat

• Those which take the system from one state to another:

	addUsrGrpToAcl
	chmod
	chobjsc
	chown
	chsubsc
	close
	create
	delUsrGrpFromAlc
	mkdir
	open
	owner_close
	rmdir
	unlink
	write

There are file system calls not explicitly described by the model. However, every file system call corresponds with some operation of the model; this information is available in the design document.

Also, there is a formal description of those security properties to be satisfied by the model. Security properties define the meaning of secure state or secure transition from different points of view. LSM 0.0 defines four different security properties:

 

	Discretionary security
	Simple security
	Confinement
	Change of security attributes

Finally, it has been formally verified that the model satisfies all the expected security properties.