@techreport{oai:ipsj.ixsq.nii.ac.jp:00021344,
 author = {中島, 震 and 玉井, 哲雄 and Shin, Nakajima and Tetsuo, Tamai},
 issue = {73(2003-SE-143)},
 month = {Jul},
 note = {セキュリティに関する考慮は、システム開発の初期段階から必要であるが、同時に、システム出荷ならびにサービスイン以降の要求事項変化に対応しなければならない。サービスイン以降の変更を容易にするために、設定ファイルに代表される宣言的な情報を修正することで要求変更に対応することが多い。しかし、現実のシステムでは、宣言的な情報だけでセキュリティ要求を実現することは難しい。アプリケーションプログラムに混在する手続き的な処理記述とあわさってはじめて所望の目的を達成することができる。セキュリティ要求の変更はプログラム変更を伴い、このような変更は当該アプリケーション機能と複雑に絡むため、適切に変更することが難しい。本稿では、アクセス管理に関するセキュリティ要求の変更をデザインの段階で取り扱う。特に、具体的な基盤としてJAASを扱う。形式手法を用いた解析を行なうため、デザインを形式仕様言語Alloy で表現する。宣言的な情報と手続き的な処理記述の双方を単一の枠組で表現・解析することで、互いの相互依存関係が明確になる。その結果、両方の観点を含む仕様記述に対する解析を行なうことが可能になる。特に、セキュリティ要求の変更に対するデザイン変更を議論する上でAlloyが有用であることを示す。, Security is one of the major design issues that we should address in early stages of the system development. In addition, the system should have an extensible security. It is because the security requirements are often changed after the system is shipped and begins daily operations. In order to easily accommodate the system to the changes, the security enforcement mechanism is sometimes implemented in the application program level as seen in Java-based systems. Although the application-based approach has the advantages in view of the extensibility, portability, and performance, it sometimes makes the design complicated. A change in the security requirement may lead to a lot of changes spread over the design. In sum, the security is a ``cross-cutting concern.'' We are interested in applying the formal specification and analysis techniques to the design regarding to the security requirements. In this paper, we argue that Alloy is shown useful for the analysis of changes in the security requirements. It owes much to the declarative specification style together with the constraint-based analysis mechanism. We present some technical details of a case using Alloy for the formal specification and analysis of JAAS.},
 title = {セキュリティポリシー変更に関するデザイン解析},
 year = {2003}
}