甲府方重信Blog

...Shigenobu Koufugatas Blog

  • Increase font size
  • Default font size
  • Decrease font size
Error
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
  • Unable to load Cache Storage: database
Home 業務日誌 Adaプログラミング Adaチュートリアル セクション17.4 - 安全性とAda

Adaチュートリアル セクション17.4 - 安全性とAda

E-mail Print PDF

セクション 17.4 - 安全性とAda

Adaは、安全性が重要な考慮点ではない領域で使われることがあることがある一方で、多くの安全性クリティカルなアプリケーションがAdaで開発されています。現在、安全性クリティカルなソフトウェアを開発する計画がない場合であっても、いくらか基本について知っておくのは良い事です。最初に、私たちはいくつかのソフトウェア安全性に関する概念を紹介します。そして、Ada固有の項目に続きます。

ソフトウェアの安全性の概観

ソフトウェアの安全性は、受付不可能なシステムリスクなしに、システムの文脈に沿ってソフトウェアが実行されることを確認することを含みます。安全性は、システム全体の資産であり、ソフトウェアにとどまるものではありません。しかし、ソフトウェア・コンポーネントはシステムの安全性を決定付ける可能性があります。リスクは、(1)災害可能性と(2)災害時に影響する災害の深刻さの関数として定義することができます。 現実の生活においては、「完全に」安全でありうることは少ないのですが、その代わりに、私たちはリスクを低減させ、受け入れ可能なレベルにすることを試みます。

ひとつ、共通した誤解は、よくテストされ、高度に信頼度が高いソフトウェアシステムは安全である、という考えです。伝統的な確認(テスト)技術は、シンプルなプログラムに対してさえ安全性クリティカルな不具合を発見することに対しては、はなはだしく不十分であることが、実験的にデモンストレーションされています。 [Gowen 1994]. このように、単純にシステムをテストすることは、安全なシステムを作成することには、つながらないのです。信頼性のあるシステムのいずれもが、安全なシステムであるとは限りません。ほとんどの時間は正常に動作するシステムが、時折、一定の範囲にいる人々を殺してしまうというのでは、通常安全であるとは考えられません。モデレートされたニュースグループ comp.risks は、ソフトウェアがねじれて、深刻な問題の原因を作る例を、継続して提供し続けています。

個人的には、私はあなたが、死に至ったり、深刻な怪我の原因となったり、もしくは重要な資産の損害を引き起こすようなソフトウェアを開発しているかもしれないと考えたとき、あなたは少し怖さを感じるべきだと思っています。もし、あなたがそうでないなら、あなたはこの問題が含む事項を理解していないのでしょう。ほんのちょっとの怖さが健康的なのであって、それはプログラマーが全体のリスクを低減するための技術を学び、使用することを推し進めることになるからです。

ソフトウェアの安全性領域の概観を与える、いくつかの良い調査報告書が Place [1993]Leveson [1991a]Leveson [1986]などです。  [Place 1993] はインターネット上で自由に閲覧可能です。

そこでは、一連の専門のハザード分析技術が安全性の問題を認識するために役に立ちます。ここでは、それらの二つを示します。:

  1. ソフトウェア・フォルト・ツリー分析 (FTA) は、システムにおいて安全性の危険度の潜在的な原因を認識するためのテクニックです。ソフトウェア FTAにおいては、安全性の危険度リスト(回避すべき条件)が最初に作成されます。 そして、アナリストは、分析の目的のために、その条件を仮定して、それぞれの危険度を(順に)発生した場合を考えます。そして、アナリストは、これらの危険度から、そのソフトウェアを通じて、未開発の作業を行うのです。ロジック・ダイアグラムを作成したり、その安全性の危険度がどのように発生するかを示すために。 (理想から言えば、アナリストはそれらの危険度が発生しないことを決定付けることができればいいのですが) このテクニックは理解しやすく、システムの安全性作業に統合しやすいのが特徴です。 Leveson [1983] は、ソフトウェアFTAについての一般的な議論を提供しています。一方、 Leveson [1991b] は、ソフトウェアFTAをAdaプログラムにどのように適用するか専門的に示しています。
  2. 安全性に関係したテクニックのもうひとつの集合は、フォーマル・メソッドと呼ばれています。 フォーマル・メソッドは、プログラム資産の定義と可能性に対する(フォーマルな)数学技術の応用です。現在、フォーマル・メソッドは、非常に多くの研究の対象となっています。しかし、現実的なプログラムの規模に適用するには、困難なため、実際にはあまり使われていません。 それでも、さまざまな程度でフォーマル・メソッドを使用しているシステムがあります。そして、時間の経過とともに適用度が増加する希望を持つ理由があります。 YAHOOは、いくつかのフォーマル・メソッドに関する情報への参照を持っています。 良く知られた記述言語には、VDMとZ (「ゼッド」と発音します)があります。

安全性に関するWebサーバーは、 The World Wide Web Virtual Library: Safety-Critical Systemsです。このWebサーバーはフォーマル・メソッドの側面を強調していますが、 しかしある程度ほかのものもカバーしています。

 

Adaとソフトウェア安全性

Adaは、しばしば安全性クリティカルなソフトウェアに使用されます。それは組み込まれた機能のためです。ここでは、いくつかの安全性クリティカルなシステムに対して特化したAdaの機能を示します。:

  1. 特定の条件下では、(整数型や数え上げ型のような)スカラー値が正式な範囲に入っているかどうかをチェックするのは重要です。たとえば、ハードウェア・エラーや、宇宙線がソフトウェアの制御外に値を変更している可能性があります。そして、ほかの言語とのインターフェースは、範囲外の値を渡すことができます。Ada 95は 「Valid to check if a value is out-of-range ('Valid is explained in RM 13.9.2)」という名前の属性を持っています。 X'Valid句は、Xが特定のスカラー値であり、Xが範囲内なら真を、そうでないなら偽となります。
  2. 安全なシステムでは、計算機言語は、正しいことを示すことを容易にする構造にしばしば制限されます。(あるいはフォーマル・メソッドを使うか、潜在的な問題を回避するかです) Pragma Restrictions (see RM 13.12) は、言語のどの部分が特定のプログラムに用いるべきでないかを記述ために使用することができます。
  3. Ada 95は、オプションとして、「Safety and Security」機能を持っており、コンパイラーに実装されていれば、安全でセキュアなプログラム開発をサポートする付加的な操作と機能を付け加えることができます。たとえば、このオプション機能は pragma Normalize_Scalarsを追加しますが、範囲外の値が可能な場合に、初期化されていない値を設定します。(このことで、初期化されていない値を発見するのを容易にします。

ここでは、安全性に制限されたAdaのサブセットの例を示します。:

  1. SPARKは、「安全な」Ada 83のサブセットであり、フォーマル・メソッドに影響され、アプローチやツールの集合に伴って、設計されています。SPARKを用いると、開発者はZ仕様書を取り、仕様書から段階的な詳細化を行い、SPARKのコードに変換します。各詳細化の段階に対しては、確認条件(VC's)を生成するためにツールが仕様されます。確認条件は、数学の定理に基づくものです。もし、この確認条件が証明されれば、詳細化の段階は有効であると確認されます。しかしながら、確認条件が証明されなかった場合には、詳細化の段階はエラーであると考えられます。 さらに詳しい情報についてはSPARKのサイトを参照してください。
  2. Pyle [1991] は、安全性の目的に対するさまざまな制限について議論、比較しています。

出典:http://www.adahome.com/Tutorials/Lovelace/s17s4.htm

Last Updated on Monday, 25 March 2013 10:06  

ニュース速報

一般向けのLinuxセキュリティー講座の3回目

 

1、Apache、メールサーバ、BINDなどのサービスのセキュリティ

2、SSHの詳細、SSLの仕組みなど

3、iptables

4、IDSの解説、tripwireの設置演習

5、rootkit対策

などの授業であった。

受講生は8名。

演習実施中に、来週のセキュリティーサーバー構築演習に必要なCentOS4.7のメディアを確認していたら、なんと、

4.7は、ネットからコンポーネントがなくなっていてネットワークインストールができなくなっていた。

急いで、CentOS 4.8のメディアを作成し、ネットワークインストールの環境を作ることに。

授業後、ネットワークインストールの確認をしていたら、帰宅が遅くなってしまった。ひやひや。