Toward Formal Verification of Role-Based.pdf접근 제어는 요즘 가장 기본적이고 범용적인 보안 매커니즘이다. 접근 제어 정책의 명세와 관리에 문제점들을 가지고 있으며 관리자들을 돕는 툴들은 거의 없다. 정책을 잘못 설정하여 보안에 많은 허점이 발생되고 있다. 관리자들은 종종 정책 설정을 변경하기를 꺼려한다. 설정 변경의 결과가 제대로 되어 있는지 확신을 가질 수 없기 때문에..
대부분의 접근제어 시스템에서 권한 을 변화시킬 필요가 있다. 예를 들어 , 사용자들과 객체들은 제거되고 추가되어 진다. 사용자들은 리소스 공유를 잠시 시작하고 다시 잠시 후 멈추고 사용자들의 업무 기능들이 변화한다. 이러한 동적인 특성은 접근 제어의 해결해야할 점이다. 접근제어의 동적인 면을 다루는데 기본적인 문제는 안정성 분석이다. (Harrison) 안정성 분석은 미래에 발생할 바람직하지 못한 누스가 발생할지를 결정한다. Security Analysis Problem은 접근 제어 시스템이 상태 변화 다르게 보안 정책 불변을 보존하고 있는지 요청한다. 보안 분석은 또한 신뢰할 대상에 대한 명세를 허락한다.??
목표는 관리자가 바람직한 보안 속성들을 유지를 어떻게 해야하는지.... 정확히 이해하도록 돕는 것이다.
