Using CQUAL for static analysis of authorization hook placement

Xiaolan Zhang; Antony Edwards; Trent Jaeger

Using CQUAL for static analysis of authorization hook placement

Xiaolan Zhang, Antony Edwards, Trent Jaeger

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The Linux Security Modules (LSM) framework is a set of authorization hooks for implementing flexible access control in the Linux kernel. While much effort has been devoted to defining the module interfaces, little attention has been paid to verifying the correctness of hook placement. This paper presents a novel approach to the verification of LSM authorization hook placement using CQUAL, a type-based static analysis tool. With a simple CQUAL lattice configuration and some GCC-based analyses, we are able to verify complete mediation of operations on key kernel data structures. Our results reveal some potential security vulnerabilities of the current LSM framework, one of which we demonstrate to be exploitable. Our experiences demonstrate that combinations of conceptually simple tools can be used to perform fairly complex analyses.

Original language	English (US)
Title of host publication	Proceedings of the 11th USENIX Security Symposium
Publisher	USENIX Association
ISBN (Electronic)	1931971005, 9781931971003
State	Published - 2002
Event	11th USENIX Security Symposium - San Francisco, United States Duration: Aug 5 2002 → Aug 9 2002

Publication series

Name	Proceedings of the 11th USENIX Security Symposium

Conference

Conference	11th USENIX Security Symposium
Country/Territory	United States
City	San Francisco
Period	8/5/02 → 8/9/02

All Science Journal Classification (ASJC) codes

Computer Networks and Communications
Information Systems
Safety, Risk, Reliability and Quality

Cite this

@inproceedings{0166b67148604d3e9e7da4be24584682,

title = "Using CQUAL for static analysis of authorization hook placement",

abstract = "The Linux Security Modules (LSM) framework is a set of authorization hooks for implementing flexible access control in the Linux kernel. While much effort has been devoted to defining the module interfaces, little attention has been paid to verifying the correctness of hook placement. This paper presents a novel approach to the verification of LSM authorization hook placement using CQUAL, a type-based static analysis tool. With a simple CQUAL lattice configuration and some GCC-based analyses, we are able to verify complete mediation of operations on key kernel data structures. Our results reveal some potential security vulnerabilities of the current LSM framework, one of which we demonstrate to be exploitable. Our experiences demonstrate that combinations of conceptually simple tools can be used to perform fairly complex analyses.",

author = "Xiaolan Zhang and Antony Edwards and Trent Jaeger",

note = "Funding Information: We would like to thank Jeff Foster from UC Berkeley for his timely responses to our numerous questions on CQUAL and for his suggestions and advices on the early draft of this paper. We also thank the anonymous reviewers for their valuable comments. Publisher Copyright: {\textcopyright} 2002 by The USENIX Association All Rights Reserved.; 11th USENIX Security Symposium ; Conference date: 05-08-2002 Through 09-08-2002",

year = "2002",

language = "English (US)",

series = "Proceedings of the 11th USENIX Security Symposium",

publisher = "USENIX Association",

booktitle = "Proceedings of the 11th USENIX Security Symposium",

}

TY - GEN

T1 - Using CQUAL for static analysis of authorization hook placement

AU - Zhang, Xiaolan

AU - Edwards, Antony

AU - Jaeger, Trent

N1 - Funding Information: We would like to thank Jeff Foster from UC Berkeley for his timely responses to our numerous questions on CQUAL and for his suggestions and advices on the early draft of this paper. We also thank the anonymous reviewers for their valuable comments. Publisher Copyright: © 2002 by The USENIX Association All Rights Reserved.

PY - 2002

Y1 - 2002

N2 - The Linux Security Modules (LSM) framework is a set of authorization hooks for implementing flexible access control in the Linux kernel. While much effort has been devoted to defining the module interfaces, little attention has been paid to verifying the correctness of hook placement. This paper presents a novel approach to the verification of LSM authorization hook placement using CQUAL, a type-based static analysis tool. With a simple CQUAL lattice configuration and some GCC-based analyses, we are able to verify complete mediation of operations on key kernel data structures. Our results reveal some potential security vulnerabilities of the current LSM framework, one of which we demonstrate to be exploitable. Our experiences demonstrate that combinations of conceptually simple tools can be used to perform fairly complex analyses.

AB - The Linux Security Modules (LSM) framework is a set of authorization hooks for implementing flexible access control in the Linux kernel. While much effort has been devoted to defining the module interfaces, little attention has been paid to verifying the correctness of hook placement. This paper presents a novel approach to the verification of LSM authorization hook placement using CQUAL, a type-based static analysis tool. With a simple CQUAL lattice configuration and some GCC-based analyses, we are able to verify complete mediation of operations on key kernel data structures. Our results reveal some potential security vulnerabilities of the current LSM framework, one of which we demonstrate to be exploitable. Our experiences demonstrate that combinations of conceptually simple tools can be used to perform fairly complex analyses.

UR - http://www.scopus.com/inward/record.url?scp=85084161756&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85084161756&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85084161756

T3 - Proceedings of the 11th USENIX Security Symposium

BT - Proceedings of the 11th USENIX Security Symposium

PB - USENIX Association

T2 - 11th USENIX Security Symposium

Y2 - 5 August 2002 through 9 August 2002

ER -

Using CQUAL for static analysis of authorization hook placement

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this