NDLI: Using build-integrated static checking to preserve correctness invariants

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

Operational experiences with high-volume network intrusion detection

On mutually-exclusive roles and separation of duty

Attacking and repairing the winZip encryption scheme

Pong-cache poisoning in GUESS

Direct anonymous attestation

IP covert timing channels: design and detection

Privacy and security in library RFID: issues, practices, and architectures

A PIN-entry method resilient against shoulder surfing

Verifying policy-based security for web services

On the effectiveness of address-space randomization

The dual receiver cryptosystem and its applications

Trusting a trusted system

On the difficulty of scalably detecting network attacks

KNOW Why your access was denied: regulating feedback for usable security

Reusable cryptographic fuzzy extractors

Web tap: detecting covert web traffic

Concealing complex policies with hidden credentials

Private inference control

Parallel mixing

New client puzzle outsourcing techniques for DoS resistance

A decision procedure for the verification of security protocols with explicit destructors

Attestation-based policy enforcement for remote access

Versatile padding schemes for joint signature and encryption

Testing network-based intrusion detection signatures using mutant exploits

Comparing the expressive power of access control models

Cryptanalysis of a provably secure CRT-RSA algorithm

On achieving software diversity for improved network security using distributed coloring algorithms

k-anonymous secret handshakes with reusable credentials

Security policies for downgrading

Fragile mixing

Mitigating bandwidth-exhaustion attacks using congestion puzzles

Using build-integrated static checking to preserve correctness invariants

Gray-box extraction of execution graphs for anomaly detection

ID-based encryption for complex hierarchies with applications to forward security and broadcast encryption

Payload attribution via hierarchical bloom filters

Group signatures with verifier-local revocation

Using build-integrated static checking to preserve correctness invariants

Content Provider	ACM Digital Library
Author	Shapiro, Jonathan S. Chen, Hao
Abstract	A key missing link in the creation of secure and robust systems is finding a ost effective way to demonstrate and preserve correspondence between a software design and its implementation. This paper explores the use of software model checking techniques to validate selected design invariants in the EROS operating system kernel. Several global consistency policies in the EROS kernel can be expressed as finite state automata. Using the MOPS static hecker, we have been able to validate the EROS kernel implementation against these automata. In the process, we have confirmed the practical utility of the basic verification technique, identified a number of desirable enhancements in MOPS, and located bugs in the EROS implementation. A key contribution of this paper is establishing that it is practical to integrate software model checking into normal development lifestyle. Model hecking is efficient enough that it does not add noticeably to our build times. This allows us to view it as a tool for error prevention rather than detection. Our work with EROS and MOPS suggests that domain specific application of software model hecking is a practical and powerful technique for software assurance and maintenance.
Starting Page	288
Ending Page	297
Page Count	10
File Format	PDF
ISBN	1581139616
DOI	10.1145/1030083.1030122
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2004-10-25
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Eros Mops Assurance Static analysis Verification Model hecking Security
Content Type	Text
Resource Type	Article

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

Using build-integrated static checking to preserve correctness invariants (2004)

MOPS: an infrastructure for examining security properties of software

Exploring static checking for software assurance (2003).

Model checking security policy model using both UML static and dynamic diagrams

Correctness witnesses: exchanging verification results between verifiers

Sufficient conditions for vertical composition of security protocols

Static Code Analysis for Software Security Verification: Problems and Approaches

Towards Practical Reactive Security Audit Using Extended Static Checkers

HW/SW Co-Verification of a RISC CPU using Bounded Model Checking

Using build-integrated static checking to preserve correctness invariants

Similar Documents

Using build-integrated static checking to preserve correctness invariants (2004)

MOPS: an infrastructure for examining security properties of software

Exploring static checking for software assurance (2003).

Model checking security policy model using both UML static and dynamic diagrams

Correctness witnesses: exchanging verification results between verifiers

Sufficient conditions for vertical composition of security protocols

Static Code Analysis for Software Security Verification: Problems and Approaches

Towards Practical Reactive Security Audit Using Extended Static Checkers

HW/SW Co-Verification of a RISC CPU using Bounded Model Checking

Using build-integrated static checking to preserve correctness invariants