Affiliations: [a] Universität Augsburg, Lehrstuhl für Softwaretechnik und Programmiersprachen, D-86135 Augsburg, Germany | [b] DFKI GmbH, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany | [c] IBM T.J. Watson Research Center, 30 Saw Mill River Rd., Hawthorne, NY 10532, USA
Note: [1] Augsburg and DFKI research sponsored by the German Information Security Agency (BSI).
Abstract: We present two generic formal security models for operating systems of multiapplicative smart cards. The models formalize the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applications. The first model is as abstract as possible, whereas the second extends the first by adding practically relevant issues such as a structured file system. The models satisfy a common security policy consisting of authentication and intransitive noninterference. The policy extends the classical security policy of Bell/LaPadula and Biba models, but avoids the need for trusted processes that are allowed to circumvent the security policy. Instead trusted processes are incorporated directly in the model itself and are subject to the security policy. The security policy has been formally proven to be correct for both models.
