Research on formal security policy model specification and its formal analysis
Formal method is one of the kernel technologies of developing high security level computer system.But by current formal development method,assurance of security policy model correctness cannot be provided directly using machine proof which is stricter than manual proof,correspondence between securit...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2006-01-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/74661080/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | Formal method is one of the kernel technologies of developing high security level computer system.But by current formal development method,assurance of security policy model correctness cannot be provided directly using machine proof which is stricter than manual proof,correspondence between security policy model and security functional specification is also hard to achieve.To solve these problems,a new and effective method was proposed for specification constructing and proving by extending the specification technique of security functional specification into the specifica-tion of security policy model.Also,BLP model was specified and analyzed as an example. |
|---|---|
| ISSN: | 1000-436X |