NDLI: Formal specification and verification of data separation in a separation kernel for an embedded system

Please wait, while we are loading the content...

Providing witness anonymity in peer-to-peer systems

Packet vaccine: black-box exploit detection and signature generation

Data collection with self-enforcing privacy

Resiliency policies in access control

Doppelganger: Better browser privacy without the bother

Forward-secure signatures with untrusted update

Puppetnets: misusing web browsers as a distributed attack infrastructure

TinySeRSync: secure and resilient time synchronization in wireless sensor networks

Replayer: automatic protocol replay by binary analysis

Formal specification and verification of data separation in a separation kernel for an embedded system

Stateful public-key cryptosystems: how to encrypt with one 160-bit exponentiation

System and network trustworthiness in perspective

Salsa: a structured approach to large-scale anonymity

Protomatching network traffic for high throughputnetwork intrusion detection

Searchable symmetric encryption: improved definitions and efficient constructions

Safety and consistency in policy-based authorization systems

Fourth-factor authentication: somebody you know

How to win the clonewars: efficient periodic n-times anonymous authentication

A natural language approach to automated cryptanalysis of two-time pads

Secure hierarchical in-network aggregation in sensor networks

EXE: automatically generating inputs of death

Beyond separation of duty: an algebra for specifying high-level security policies

Multi-signatures in the plain public-Key model and a general forking lemma

Hot or not: revealing hidden services by their clock skew

Evading network anomaly detection systems: formal reasoning and practical techniques

Attribute-based encryption for fine-grained access control of encrypted data

On the modeling and analysis of obligations

An effective defense against email spam laundering

A fully collusion resistant broadcast, trace, and revoke system

Dictionary attacks using keyboard acoustic emanations

Provably-secure time-bound hierarchical key assignment schemes

A scalable approach to attack graph generation

Computationally sound secrecy proofs by mechanized flow analysis

Deniable authentication and key exchange

Secure attribute-based systems

RoleMiner: mining roles using subset enumeration

Inferring the source of encrypted HTTP connections

Optimizing BGP security by exploiting path stability

Secure function evaluation with ordered binary decision diagrams

Formal specification and verification of data separation in a separation kernel for an embedded system

Content Provider	ACM Digital Library
Author	Heitmeyer, Constance L. McLean, John Archer, Myla Leonard, Elizabeth I.
Abstract	Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to rea-son about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded soft-ware system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of dataseparation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.
Starting Page	346
Ending Page	355
Page Count	10
File Format	PDF
ISBN	1595935185
DOI	10.1145/1180405.1180448
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2006-10-30
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Theorem proving Formal specification Separation kernel Formal model Code verification
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in