Loading article…
コンピュータ科学において、言語ベースセキュリティ（LBS）とは、プログラミング言語の特性を利用してアプリケーションのセキュリティを高度なレベルで強化するために用いられる一連の技術である。LBSは、アプリケーションレベルでコンピュータセキュリティを強化するものと考えられており、従来のオペレーティングシステムのセキュリティでは対処できない脆弱性を防止することを可能にする。
ソフトウェアアプリケーションは通常、特定のプログラミング言語で仕様が定められ、実装されます。アプリケーションのソースコードが攻撃、欠陥、バグの影響を受けやすい場合、それらから保護するためには、アプリケーションレベルのセキュリティが必要となります。これは、プログラミング言語に基づいてアプリケーションの動作を評価するセキュリティです。この分野は一般的に言語ベースのセキュリティと呼ばれています。
SCADAなどの大規模ソフトウェアシステムの利用は世界中で行われており[ 1 ]、コンピュータシステムは多くのインフラストラクチャの中核を成しています。社会は水、エネルギー、通信、輸送などのインフラストラクチャに大きく依存しており、これらはすべて完全に機能するコンピュータシステムに依存しています。ソフトウェアのバグやエラーにより重要なシステムが故障した有名な例がいくつかあります。たとえば、コンピュータのメモリ不足により LAX のコンピュータがクラッシュし、数百便のフライトが遅延した(2014 年 4 月 30 日) などです。[ 2 ] [ 3 ]
従来、ソフトウェアの正しい動作を制御するメカニズムは、オペレーティングシステムレベルで実装されてきました。オペレーティングシステムは、メモリアクセス違反、スタックオーバーフロー違反、アクセス制御違反など、さまざまなセキュリティ違反を処理します。これはコンピュータシステムのセキュリティにおいて非常に重要な部分ですが、ソフトウェアの動作をより具体的なレベルで保護することで、さらに強力なセキュリティを実現できます。コンパイル時にソフトウェアの多くの特性や動作が失われるため、マシンコードの脆弱性を検出することは非常に困難です。コンパイル前にソースコードを評価することで、プログラミング言語の理論と実装も考慮に入れることができ、より多くの脆弱性を発見できます。
「では、なぜ開発者は同じ過ちを繰り返すのでしょうか？プログラマーの記憶に頼るのではなく、一般的なセキュリティ脆弱性に関する既知の情報を体系化し、開発プロセスに直接統合するツールを開発するよう努めるべきです。」
— D. エヴァンスと D. ラロシェル、2002 年
LBS（ローカルベースセキュリティ）を用いることで、使用する技術に応じて、ソフトウェアのセキュリティを様々な面で向上させることができます。バッファオーバーフローや不正な情報フローの発生を許容するなど、一般的なプログラミングエラーを検知し、ユーザーが使用するソフトウェア内で発生しないようにすることが可能です。また、ソフトウェアのセキュリティ特性についてユーザーに何らかの証明を提供することも望ましいでしょう。これにより、ユーザーはソースコードを入手してエラーを自己チェックすることなく、ソフトウェアを信頼できるようになります。
コンパイラは、ソースコードを入力として受け取り、そのコードを機械可読コードに変換するために、言語固有の様々な処理を実行します。字句解析、前処理、構文解析、意味解析、コード生成、コード最適化は、コンパイラで一般的に用いられる処理です。コンパイラは、ソースコードを分析し、言語の理論と実装を活用することで、プログラムの動作を維持しながら、高水準コードを低水準コードに正しく変換しようと試みます。
Javaなどの型安全な言語で書かれたプログラムをコンパイルする際、ソースコードはコンパイル前に型チェックに合格する必要があります。型チェックに合格しない場合、コンパイルは実行されず、ソースコードを修正する必要があります。つまり、適切なコンパイラを使用すれば、型チェックに合格したソースプログラムからコンパイルされたコードには、無効な代入エラーは含まれないはずです。これは、特定のエラーによってプログラムがクラッシュしないという一定の保証となるため、コード利用者にとって有益な情報となります。
LBSの目標の一つは、ソフトウェアの安全ポリシーに対応する特定の特性がソースコードに存在することを保証することです。コンパイル中に収集された情報は、当該プログラムの安全性を証明する証明書を作成するために使用され、その証明書は消費者に提供されます。このような証明は、消費者が供給者が使用するコンパイラを信頼できること、そしてソースコードに関する情報である証明書が検証可能であることを示唆するものでなければなりません。
この図は、認証コンパイラを使用することで、低レベルコードの認証と検証をどのように実現できるかを示しています。ソフトウェア供給者はソースコードを公開する必要がないという利点を得られ、消費者は証明書の検証という作業のみを行うことになります。これは、ソースコード自体の評価やコンパイルに比べれば容易な作業です。証明書の検証には、コンパイラと検証ツールを含む限定された信頼できるコードベースのみが必要です。
プログラム解析の主な用途は、プログラムの最適化（実行時間、メモリ使用量、消費電力など）とプログラムの正当性（バグ、セキュリティ脆弱性など）です。プログラム解析は、コンパイル時（静的解析）、実行時（動的解析）、またはその両方に適用できます。言語ベースのセキュリティにおいては、プログラム解析は、型チェック（静的および動的）、監視、汚染チェック、制御フロー解析など、いくつかの有用な機能を提供できます。
情報フロー分析とは、通常のアクセス制御メカニズムでは不十分な場合に、機密性と完全性を維持するために、プログラム内の情報フロー制御を分析するために使用される一連のツールと説明できます。
「情報へのアクセス権と情報発信権を切り離すことで、フローモデルはアクセスマトリックスモデルを凌駕し、安全な情報フローを規定する能力を高めている。実用的なシステムでは、すべてのセキュリティ要件を満たすために、アクセス制御とフロー制御の両方が必要となる。」
— D. デニング、1976年
アクセス制御は情報へのアクセスに対するチェックを強制しますが、その後に何が起こるかについては考慮しません。例を挙げます。あるシステムにアリスとボブという2人のユーザーがいます。アリスはsecret.txtというファイルを持っており、これはアリスのみが読み取りと編集を許可されており、アリスはこの情報を自分だけのものにしておきたいと考えています。システムにはpublic.txtというファイルもあり、これはシステム内のすべてのユーザーが自由に読み取りと編集を行うことができます。ここで、アリスが誤って悪意のあるプログラムをダウンロードしたとします。このプログラムはアリスとしてシステムにアクセスでき、secret.txtに対するアクセス制御チェックを回避します。そして、悪意のあるプログラムはsecret.txtの内容をコピーしてpublic.txtに配置し、ボブや他のすべてのユーザーがそれを読めるようにします。これは、システムの意図された機密性ポリシーに違反します。
非干渉性とは、セキュリティ分類の低い変数の入力に応じて、セキュリティ分類の高い変数の情報が漏洩したり、明らかにされたりしないというプログラムの特性です。非干渉性を満たすプログラムは、対応する下位変数に同じ入力が与えられた場合、常に同じ出力を生成する必要があります。これは、入力のあらゆる値に対して成り立つ必要があります。つまり、プログラム内の上位変数が実行ごとに異なる値を持つ場合でも、下位変数にはその影響が現れないということです。
攻撃者は、非干渉条件を満たさないプログラムを繰り返し体系的に実行することで、その動作を解明しようとする可能性がある。これを何度か繰り返すと、上位変数が漏洩し、例えばシステムの状態に関する機密情報が明らかになる可能性がある。
セキュリティタイプのシステムが存在することを前提として、プログラムが非干渉性を満たしているかどうかはコンパイル中に評価できます。
セキュリティ型システムとは、ソフトウェア開発者がコードのセキュリティ特性を検証するために使用できる型システムの一種です。セキュリティ型を備えた言語では、変数と式の型はアプリケーションのセキュリティポリシーに関連付けられ、プログラマは型宣言によってアプリケーションのセキュリティポリシーを指定できます。型は、認可ポリシー（アクセス制御や機能など）や情報フローセキュリティなど、さまざまな種類のセキュリティポリシーについて推論するために使用できます。セキュリティ型システムは、基盤となるセキュリティポリシーと形式的に関連付けることができ、型チェックを行うすべてのプログラムが意味的にポリシーを満たす場合、セキュリティ型システムは健全であると言えます。たとえば、情報フローのためのセキュリティ型システムは、非干渉を強制する場合があります。これは、型チェックによって、プログラムに機密性や完全性の違反がないかどうかが明らかになることを意味します。
低レベルコードの脆弱性とは、プログラムをソースプログラミング言語では定義できない状態に陥らせるバグや欠陥のことです。低レベルプログラムの動作は、コンパイラ、ランタイムシステム、またはオペレーティングシステムの詳細に依存します。これにより、攻撃者はプログラムを未定義の状態に誘導し、システムの動作を悪用することが可能になります。
安全性の低い低レベルコードの一般的な脆弱性を悪用すると、攻撃者はメモリ アドレスへの不正な読み書きを実行できます。メモリ アドレスはランダムな場合もあれば、攻撃者によって選択される場合もあります。
安全な低レベルコードを実現するアプローチの一つは、安全な高レベル言語を使用することです。安全な言語は、プログラマのマニュアルによって完全に定義されていると考えられています。[ 4 ]安全な言語で実装依存の動作を引き起こす可能性のあるバグは、コンパイル時に検出されるか、実行時に明確に定義されたエラー動作につながります。Java では、配列の範囲外にアクセスすると例外がスローされます。その他の安全な言語の例としては、C#、Haskell、Scalaなどがあります。
安全でない言語のコンパイル時には、ソースレベルの未定義動作を検出するために、低レベルコードに実行時チェックが追加されます。例えば、境界違反が検出された場合にプログラムを終了させるカナリアの使用が挙げられます。境界チェックなどの実行時チェックを使用する際の欠点は、パフォーマンスにかなりのオーバーヘッドが発生することです。
実行不可能なスタックやヒープの使用といったメモリ保護は、追加の実行時チェックとみなすこともできます。これは多くの最新のオペレーティングシステムで採用されています。
基本的な考え方は、ソースコードを分析することで、アプリケーションデータから機密性の高いコードを特定することです。この分析が完了すると、異なるデータが分離され、それぞれ別のモジュールに配置されます。各モジュールが、自身に含まれる機密情報を完全に制御できると仮定すれば、いつ、どのようにモジュールから情報が送信されるかを指定することが可能です。例えば、暗号化モジュールでは、暗号化されていない鍵がモジュールから送信されることを防止できます。
コンパイル認証とは、高水準プログラミング言語のセマンティクス情報を用いて、ソースコードのコンパイル中に証明書を生成するという考え方です。この証明書はコンパイル済みコードに同梱され、ソースコードが特定のルールに従ってコンパイルされたことを利用者に証明する役割を果たします。証明書は、例えば証明コード（PCC）や型付きアセンブリ言語（TAL）など、様々な方法で生成できます。
PCCの主な側面は、以下のステップにまとめられます。[ 5 ]
認証コンパイラの一例として、Touchstoneコンパイラが挙げられる。これは、Javaで実装されたプログラムに対して、型安全性とメモリ安全性のPCC形式証明を提供する。
TALは、型システムを利用するプログラミング言語に適用可能です。コンパイル後、オブジェクトコードには、通常の型チェッカーでチェック可能な型注釈が付加されます。ここで生成される注釈は、いくつかの制限はあるものの、PCCが提供する注釈と多くの点で類似しています。しかし、TALは、メモリ安全性や制御フローなど、型システムの制約によって表現されるあらゆるセキュリティポリシーに対応できます。
{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）