More Web Proxy on the site http://driver.im/

Article

Verifying Information Flow Control over Unbounded Processes

Authors:

William R. Harris,

Nicholas A. Kidd,

Thomas RepsAuthors Info & Claims

FM '09: Proceedings of the 2nd World Congress on Formal Methods

Pages 773 - 789

https://doi.org/10.1007/978-3-642-05089-3_49

Published: 04 November 2009 Publication History

Abstract

<em>Decentralized Information Flow Control</em> (DIFC) systems enable programmers to express a desired DIFC policy, and to have the policy enforced via a reference monitor that restricts interactions between system objects, such as processes and files. Past research on DIFC systems focused on the reference-monitor implementation, and assumed that the desired DIFC policy is correctly specified. The focus of this paper is an automatic technique to verify that an application, plus its calls to DIFC primitives, does indeed correctly implement a desired policy. We present an abstraction that allows a model checker to reason soundly about DIFC programs that manipulate potentially unbounded sets of processes, principals, and communication channels. We implemented our approach and evaluated it on a set of real-world programs.

References

[1]

Efstathopoulos, P., Krohn, M., VanDeBogart, S., Frey, C., Ziegler, D., Kohler, E., Mazières, D., Kaashoek, F., Morris, R.: Labels and event processes in the Asbestos operating system. SIGOPS Oper. Syst. Rev. 39(5), 17-30 (2005).

[2]

Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: OSDI (2006).

[3]

Krohn, M., Yip, A., Brodsky, M., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard os abstractions. In: SOSP (2007).

[4]

Conover, M.: Analysis of the Windows Vista Security Model. Technical report, Symantec Corporation (2008).

[5]

Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. Form. Methods Syst. Des. 25(2-3), 129-166 (2004).

[6]

Kidd, N.A., Reps, T.W., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 198-213. Springer, Heidelberg (2009).

[7]

Apache: Apache, http://www.apache.org

[8]

ClamAV: ClamAV, http://www.clamav.net

[9]

OpenVPN: OpenVPN, http://www.openvpn.net

[10]

Chaudhuri, A., Naldurg, P., Rajamani, S.K., Ramalingam, G., Velaga, L.: EON: Modeling and analyzing dynamic access control systems with logic programs. In: CCS (2008).

[11]

Krohn, M., Tromer, E.: Non-interference for a practical DIFC-based operating system. In: IEEE Symposium on Security and Privacy (2009).

[12]

Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217-298 (2002).

[13]

Harris, W.R., Kidd, N.A., Chaki, S., Jha, S., Reps, T.: Verifying information flow control over unbounded processes. Technical Report UW-CS-TR-1655, Univ. of Wisc (May 2009).

[14]

Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs (2002).

[15]

MoinMoin: The MoinMoin wiki engine (December 2006), http://moinmoin.wikiwikiweb.de

[16]

Vandebogart, S., Efstathopoulos, P., Kohler, E., Krohn, M., Frey, C., Ziegler, D., Kaashoek, F., Morris, R., Mazières, D.: Labels and Event Processes in the Asbestos Operating System. ACM Trans. Comput. Syst. 25(4), 11 (2007).

[17]

Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: POPL (2001).

[18]

Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504-513 (1977).

[19]

Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL (1999).

[20]

Guttman, J.D., Herzog, A.L., Ramsdell, J.D., Skorupka, C.W.: Verifying Information-Flow Goals in Security-Enhanced Linux. Journal of Computer Security (2005).

[21]

Zhang, X., Edwards, A., Jaeger, T.: Using CQUAL for static analysis of authorization hook placement. In: USENIX Security Symposium, pp. 33-48 (2002).

Cited By

Yuan ZLi WYang ZSun LDu XZhang H(2021)A Noninterference Model for Mobile OS Information Flow Control and Its Policy VerificationSecurity and Communication Networks10.1155/2021/24818182021Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1155/2021/2481818
Shu RWang PGorski III SAndow BNadkarni ADeshotels LGionta JEnck WGu X(2016)A Study of Security Isolation TechniquesACM Computing Surveys10.1145/298854549:3(1-37)Online publication date: 12-Oct-2016
https://dl.acm.org/doi/10.1145/2988545
Accorsi RLehmann ALohmann N(2015)Information leak detection in business process modelsInformation Systems10.1016/j.is.2013.12.00647:C(244-257)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1016/j.is.2013.12.006
Show More Cited By

Verifying Information Flow Control over Unbounded Processes
1. Software and its engineering
  1. Software creation and management

Recommendations

Securing untrustworthy software using information flow control
Nonmalleable Information Flow Control
CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

Noninterference is a popular semantic security condition because it offers strong end-to-end guarantees, it is inherently compositional, and it can be enforced using a simple security type system. Unfortunately, it is too restrictive for real systems. ...
Language-based information-flow security

Current standard security practices do not provide substantial assurance that the end-to-end behavior of a computing system satisfies important security policies such as confidentiality. An end-to-end confidentiality policy might assert that secret ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FM '09: Proceedings of the 2nd World Congress on Formal Methods

November 2009

818 pages

ISBN:9783642050886

Editors:
Ana Cavalcanti
Department of Computer Science, Heslington, University of York, York, UK Y010 5DD
,
Dennis R. Dams
Bell Laboratories, Murray Hill, USA 07974

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 04 November 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yuan ZLi WYang ZSun LDu XZhang H(2021)A Noninterference Model for Mobile OS Information Flow Control and Its Policy VerificationSecurity and Communication Networks10.1155/2021/24818182021Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.1155/2021/2481818
Shu RWang PGorski III SAndow BNadkarni ADeshotels LGionta JEnck WGu X(2016)A Study of Security Isolation TechniquesACM Computing Surveys10.1145/298854549:3(1-37)Online publication date: 12-Oct-2016
https://dl.acm.org/doi/10.1145/2988545
Accorsi RLehmann ALohmann N(2015)Information leak detection in business process modelsInformation Systems10.1016/j.is.2013.12.00647:C(244-257)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1016/j.is.2013.12.006
Accorsi RLehmann A(2012)Automatic information flow analysis of business process modelsProceedings of the 10th international conference on Business Process Management10.1007/978-3-642-32885-5_13(172-187)Online publication date: 3-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-32885-5_13
Harris WJha SReps T(2012)Secure programming via visibly pushdown safety gamesProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_41(581-598)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_41
Kidd NReps TDolby JVaziri M(2011)Finding concurrency-related bugs using random isolationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220897.322109513:6(495-518)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.5555/3220897.3221095
Yang ZYin LDuan MJin SChen YDanezis GShmatikov V(2011)PosterProceedings of the 18th ACM conference on Computer and communications security10.1145/2046707.2093515(873-876)Online publication date: 17-Oct-2011
https://dl.acm.org/doi/10.1145/2046707.2093515
Harris WJha SReps TAl-Shaer EKeromytis AShmatikov V(2010)DIFC programs by automatic instrumentationProceedings of the 17th ACM conference on Computer and communications security10.1145/1866307.1866340(284-296)Online publication date: 4-Oct-2010
https://dl.acm.org/doi/10.1145/1866307.1866340

View Options

View options

Figures

Tables

Media

View Table of Conten