A Verified Capability-Based Model for Information Flow Security With Dynamic Policies
Formal verification of information flow security with dynamic policies of security-critical systems is a grand challenge. This paper presents the first effort to formally specify and verify a capability-based system model with dynamic information flow policies. We build a generic security model with...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2018-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8315441/ |
| _version_ | 1819171977957474304 |
|---|---|
| author | Jianwen Sun Xiang Long Yongwang Zhao |
| author_facet | Jianwen Sun Xiang Long Yongwang Zhao |
| author_sort | Jianwen Sun |
| collection | DOAJ |
| description | Formal verification of information flow security with dynamic policies of security-critical systems is a grand challenge. This paper presents the first effort to formally specify and verify a capability-based system model with dynamic information flow policies. We build a generic security model with dynamic security policies. In the security model, we define a set of information flow security properties and provide an inference framework for them. Based on the security model, we propose a system model for capability-based secure systems. The system model specifies critical events including system initialization, inter-domain communication, and capability management. We prove information flow security of the capability-based model by an unwinding theorem. Formal specification and security proof are carried out in the Isabelle/HOL theorem prover and could be applied to formally develop and verify the security of capability-based secure systems, such as separation kernels and secure hypervisors. To our knowledge, this is the first machine-checked proof of capability-based information security with dynamic policies. |
| first_indexed | 2024-12-22T19:59:52Z |
| format | Article |
| id | doaj.art-3ec73b074d764ccbad81bc18d7cc5310 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-22T19:59:52Z |
| publishDate | 2018-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-3ec73b074d764ccbad81bc18d7cc53102022-12-21T18:14:18ZengIEEEIEEE Access2169-35362018-01-016163951640710.1109/ACCESS.2018.28157668315441A Verified Capability-Based Model for Information Flow Security With Dynamic PoliciesJianwen Sun0Xiang Long1Yongwang Zhao2https://orcid.org/0000-0002-2284-1383State Key Laboratory of Virtual Reality Technology and System, School of Computer Science and Engineering, Beihang University, Beijing, ChinaState Key Laboratory of Virtual Reality Technology and System, School of Computer Science and Engineering, Beihang University, Beijing, ChinaBeijing Advanced Innovation Center for Big Data and Brain Computing, Beihang University, Beijing, ChinaFormal verification of information flow security with dynamic policies of security-critical systems is a grand challenge. This paper presents the first effort to formally specify and verify a capability-based system model with dynamic information flow policies. We build a generic security model with dynamic security policies. In the security model, we define a set of information flow security properties and provide an inference framework for them. Based on the security model, we propose a system model for capability-based secure systems. The system model specifies critical events including system initialization, inter-domain communication, and capability management. We prove information flow security of the capability-based model by an unwinding theorem. Formal specification and security proof are carried out in the Isabelle/HOL theorem prover and could be applied to formally develop and verify the security of capability-based secure systems, such as separation kernels and secure hypervisors. To our knowledge, this is the first machine-checked proof of capability-based information security with dynamic policies.https://ieeexplore.ieee.org/document/8315441/Information flow securitydynamic noninterferencecapabilityformal specificationIsabelle/HOLtheorem proving |
| spellingShingle | Jianwen Sun Xiang Long Yongwang Zhao A Verified Capability-Based Model for Information Flow Security With Dynamic Policies IEEE Access Information flow security dynamic noninterference capability formal specification Isabelle/HOL theorem proving |
| title | A Verified Capability-Based Model for Information Flow Security With Dynamic Policies |
| title_full | A Verified Capability-Based Model for Information Flow Security With Dynamic Policies |
| title_fullStr | A Verified Capability-Based Model for Information Flow Security With Dynamic Policies |
| title_full_unstemmed | A Verified Capability-Based Model for Information Flow Security With Dynamic Policies |
| title_short | A Verified Capability-Based Model for Information Flow Security With Dynamic Policies |
| title_sort | verified capability based model for information flow security with dynamic policies |
| topic | Information flow security dynamic noninterference capability formal specification Isabelle/HOL theorem proving |
| url | https://ieeexplore.ieee.org/document/8315441/ |
| work_keys_str_mv | AT jianwensun averifiedcapabilitybasedmodelforinformationflowsecuritywithdynamicpolicies AT xianglong averifiedcapabilitybasedmodelforinformationflowsecuritywithdynamicpolicies AT yongwangzhao averifiedcapabilitybasedmodelforinformationflowsecuritywithdynamicpolicies AT jianwensun verifiedcapabilitybasedmodelforinformationflowsecuritywithdynamicpolicies AT xianglong verifiedcapabilitybasedmodelforinformationflowsecuritywithdynamicpolicies AT yongwangzhao verifiedcapabilitybasedmodelforinformationflowsecuritywithdynamicpolicies |