(57)【要約】  プログラムコードについてチェックを行う方法及び装置。一実施形態において、この方法は、プログラムコードを受け取るステップと、プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証するステップであって、プログラムコードにおける１つ以上の動的なチェックの各々がプログラムコードにおけるオペレーションをチェックするようなステップと、を備えている。【選択図】  図１【特許請求の範囲】
【請求項１】
プログラムコードを受け取るステップと、
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証するステップであって、前記プログラムコードにおける１つ以上の動的なチェックの各々が前記プログラムコードにおけるオペレーションをチェックするようなステップと、
を備える方法。
【請求項２】
前記動的なチェックの少なくとも１つは、オペレーションが非安全であるかどうか決定する、請求項１に記載の方法。
【請求項３】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、ランタイムの前に遂行される、請求項１に記載の方法。
【請求項４】
前記プログラムコードにおける１つ以上の動的なチェックに関してランタイムの前に情報を静的に検証する前記ステップは、安全性をチェックするためのものである、請求項１に記載の方法。
【請求項５】
前記１つ以上の動的なチェックの少なくとも１つは、リソース予約を指定するための１つ以上の注釈を含む、請求項１に記載の方法。
【請求項６】
前記リソース予約は、前記プログラムコードを安全に実行することに関連する、請求項５に記載の方法。
【請求項７】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが、ランタイム中に１つ以上のリソースのうち、前記プログラムコードが実行前に予約したものより多くを使用するかどうかチェックすることを含む、請求項１に記載の方法。
【請求項８】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが所定量より多くのリソースを使用するかどうかチェックすることを含む、請求項１に記載の方法。
【請求項９】
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、１つ以上のリソースを予約するために前記プログラムコードにおける第１セットのオペレーションの１つ以上を静的にチェックして、それら１つ以上のオペレーションにより予約される１つ以上のリソースが、前記プログラムコードにおいてリソースを消費する全てのランタイムオペレーションを考慮するに充分であるかどうか決定することを含む、請求項１に記載の方法。
【請求項１０】
１つ以上の動的なチェックを前記プログラムコードに追加するステップを更に備える、請求項１に記載の方法。
【請求項１１】
１つ以上の注釈を前記プログラムコードに追加するステップを更に備え、前記１つ以上の注釈の少なくとも１つは、前記プログラムコードの一部分により使用するためにリソースを予約するオペレーションを含む、請求項１に記載の方法。
【請求項１２】
少なくとも１つの静的なチェック及び少なくとも１つの動的なチェックの組合せを選択するステップと、
前記静的及び動的チェックを表すように前記プログラムコードに注釈を追加するステップと、
を更に備える請求項１１に記載の方法。
【請求項１３】
ランタイム中に前記動的チェックを呼び出すことにより前記プログラムコードの動的チェックを遂行するステップを更に備える、請求項１に記載の方法。
【請求項１４】
リソース使用が限界を越えたという決定に応答して前記プログラムコードによるリソース使用を制限するステップを更に備える、請求項１３に記載の方法。
【請求項１５】
前記プログラムコードによるリソース使用を制限する前記ステップは、前記プログラムコードの実行を停止する段階を含む、請求項１４に記載の方法。
【請求項１６】
リソース使用が限界を越えたという決定に応答して例外を生じさせるステップを更に備える、請求項１３に記載の方法。
【請求項１７】
リソース使用が限界を越えたという決定に応答して割り込みを発生するステップを更に備える、請求項１３に記載の方法。
【請求項１８】
前記１つ以上の動的なチェックの少なくとも１つは、リソースの使用をチェックするためのものである、請求項１に記載の方法。
【請求項１９】
前記リソースは物理的なリソースを含む、請求項１８に記載の方法。
【請求項２０】
前記物理的なリソースは、中央処理ユニット（ＣＰＵ）のインストラクションカウント、メモリスペース、ディスクスペース、ネットワーク帯域巾、装置ハードウェアオペレーション、及び装置ソフトウェアオペレーションより成るグループから選択されたものを含む、請求項１９に記載の方法。
【請求項２１】
前記リソースは仮想リソースを含む、請求項１８に記載の方法。
【請求項２２】
前記仮想リソースは、ファイルハンドル、プロセス、及びデータベース接続より成るグループから選択されたものを含む、請求項２１に記載の方法。
【請求項２３】
システムにより実行されたときに、システムが、
プログラムコードを受け取るステップと、
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証するステップであって、前記プログラムコードにおける１つ以上の動的なチェックの各々が前記プログラムコードにおけるオペレーションをチェックするためのものであるステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項２４】
前記動的なチェックの少なくとも１つは、オペレーションが非安全であるかどうか決定する、請求項２３に記載の製造物品。
【請求項２５】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、ランタイムの前に遂行される、請求項２３に記載の製造物品。
【請求項２６】
前記プログラムコードにおける１つ以上の動的なチェックに関してランタイムの前に情報を静的に検証する前記ステップは、安全性をチェックするためのものである、請求項２３に記載の製造物品。
【請求項２７】
前記１つ以上の動的なチェックの少なくとも１つは、リソース予約を指定するための１つ以上の注釈を含む、請求項２３に記載の製造物品。
【請求項２８】
前記リソース予約は、前記プログラムコードを安全に実行することに関連する、請求項２７に記載の製造物品。
【請求項２９】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが、ランタイム中に１つ以上のリソースのうち、前記プログラムコードが実行前に予約したものより多くを使用するかどうかチェックすることを含む、請求項２３に記載の製造物品。
【請求項３０】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが所定量より多くのリソースを使用しようとするかどうかチェックすることを含む、請求項２３に記載の製造物品。
【請求項３１】
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、１つ以上のリソースを予約するために前記プログラムコードにおける第１セットのオペレーションの１つ以上を静的にチェックして、それら１つ以上のオペレーションにより予約される１つ以上のリソースが、前記プログラムコードにおいてリソースを消費する全てのランタイムオペレーションを考慮するに充分であるかどうか決定することを含む、請求項２３に記載の製造物品。
【請求項３２】
前記方法は、１つ以上の動的なチェックを前記プログラムコードに追加するステップを更に備える、請求項２３に記載の製造物品。
【請求項３３】
前記方法は、１つ以上の注釈を前記プログラムコードに追加するステップを更に備え、前記１つ以上の注釈の少なくとも１つは、前記プログラムコードの一部分により使用するためにリソースを予約するオペレーションを含む、請求項２３に記載の製造物品。
【請求項３４】
前記方法は、
少なくとも１つの静的なチェック及び少なくとも１つの動的なチェックの組合せを選択するステップと、
前記静的及び動的チェックを表すように前記プログラムコードに注釈を追加するステップと、
を更に備える請求項３３に記載の製造物品。
【請求項３５】
前記方法は、ランタイム中に前記動的チェックを呼び出すことにより前記プログラムコードの動的チェックを遂行するステップを更に備える、請求項２３に記載の製造物品。
【請求項３６】
前記方法は、リソース使用が限界を越えたという決定に応答して前記プログラムコードによるリソース使用を制限するステップを更に備える、請求項３５に記載の製造物品。
【請求項３７】
前記プログラムコードによるリソース使用を制限する前記ステップは、前記プログラムコードの実行を停止することを含む、請求項３６に記載の製造物品。
【請求項３８】
前記方法は、リソース使用が限界を越えたという決定に応答して例外を生じさせるステップを更に備える、請求項３５に記載の製造物品。
【請求項３９】
前記方法は、リソース使用が限界を越えたという決定に応答して割り込みを発生するステップを更に備える、請求項３５に記載の製造物品。
【請求項４０】
前記１つ以上の動的なチェックの少なくとも１つは、リソースの使用をチェックするためのものである、請求項２３に記載の製造物品。
【請求項４１】
前記リソースは物理的なリソースを含む、請求項４０に記載の製造物品。
【請求項４２】
前記物理的なリソースは、中央処理ユニット（ＣＰＵ）のインストラクションカウント、メモリスペース、ディスクスペース、ネットワーク帯域巾、装置ハードウェアオペレーション、及び装置ソフトウェアオペレーションより成るグループから選択されたものを含む、請求項４１に記載の製造物品。
【請求項４３】
前記リソースは仮想リソースを含む、請求項４０に記載の製造物品。
【請求項４４】
前記仮想リソースは、ファイルハンドル、及びプロセスより成るグループから選択されたものを含む、請求項４３に記載の製造物品。
【請求項４５】
リソースの式を静的に決定するステップと、
実行中にプログラムコードによるリソースの使用が限度内となるかどうかチェックできるようにする１つ以上の注釈を前記プログラムコードに追加するステップと、
を備えた方法。
【請求項４６】
前記限度は割当量によりセットされる、請求項４５に記載の方法。
【請求項４７】
システムにより実行されたときに、システムが、
リソースの式を静的に決定するステップと、
実行中にプログラムコードによるリソースの使用が限度内となるかどうかチェックできるようにする１つ以上の注釈を前記プログラムコードに追加するステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項４８】
注釈を有するプログラムコードを受け取るステップと、
取得したリソースが割当量より少ないかどうかチェックすることにより、前記プログラムコードを実行する間にリソース使用をチェックするステップと、
を備える方法。
【請求項４９】
前記プログラムコードにおける１つ以上の動的チェックに関する情報は、実行の前に静的に検証されている、請求項４８に記載の方法。
【請求項５０】
前記プログラムコードにおける１つ以上の動的チェックに関する情報は、１つ以上の動的チェックの各々に関連したプログラムコードにおけるオペレーションの実行前に静的に検証されている、請求項４８に記載の方法。
【請求項５１】
前記割当量はオペレーティングシステムからのものである、請求項４８に記載の方法。
【請求項５２】
前記割当量はポリシーからのものである、請求項４８に記載の方法。
【請求項５３】
前記ポリシーは、前記プログラムコードが使用することを許された１つ以上のリソースと、前記プログラムコードにより使用してもよい１つ以上のリソース各々の量を指示する、１つ以上のリソース各々の使用限界とを指定する、請求項４８に記載の方法。
【請求項５４】
前記１つ以上のリソースの少なくとも１つに対する使用限界は、上限である、請求項４８に記載の方法。
【請求項５５】
前記１つ以上のリソースの少なくとも１つに対する使用限界は、下限である、請求項４８に記載の方法。
【請求項５６】
前記１つ以上のリソースの少なくとも１つに対する使用率は、レートである、請求項４８に記載の方法。
【請求項５７】
システムにより実行されたときに、システムが、
注釈を有するプログラムコードをダウンロードするステップと、
取得したリソースが割当量より少ないかどうかチェックすることにより、前記プログラムコードを実行する間にリソース使用をチェックするステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項５８】
ランタイム中に１つ以上のリソースの使用を動的に要求するプログラムコードを受け取るステップと、
前記プログラムコードを静的にチェックして、前記プログラムコードがランタイム中に許可されたリソースしか使用しないことを決定するステップと、
を備える方法。
【請求項５９】
システムにより実行されたときに、システムが、
ランタイム中に１つ以上のリソースの使用を動的に要求するプログラムコードを受け取るステップと、
前記プログラムコードを静的にチェックして、前記プログラムコードがランタイム中に許可されたリソースしか使用しないことを決定するステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項６０】
プログラムコードが、実行中に１つ以上のリソースのうち、前記プログラムコードが実行前に予約したものより多くを使用するかどうかチェックするためのベリファイアを備え、該ベリファイアが、
前記プログラムコードの安全条件を計算するための安全条件ジェネレータと、
前記安全条件が有効であるかどうかチェックするためのプルーフチェッカーと、
を含むものであるアーキテクチャー。
【請求項６１】
前記ベリファイアは、前記プログラムコードにおけるリソースの消費に一部分基づいて前記チェックを遂行する、請求項６０に記載のアーキテクチャー。
【請求項６２】
前記プログラムコードにおけるオペレーションにより解放されるリソースは、前記オペレーションにより解除される１つ以上のリソースを含む、請求項６１に記載のアーキテクチャー。
【請求項６３】
前記プログラムコードにおけるオペレーションにより解放されるリソースは、前記オペレーションによりリサイクルされる１つ以上のリソースを含む、請求項６１に記載のアーキテクチャー。
【請求項６４】
前記安全条件は、前記注釈を満足し且つリソース使用に関して安全である全プログラムを前記安全条件が捕獲するときに最適である、請求項６０に記載のアーキテクチャー。
【請求項６５】
プローバーを備え、該プローバーが、
プログラムコードの安全条件を計算するための安全条件ジェネレータと、
プルーフコンストラクターと、
を含むものであるアーキテクチャー。
【発明の詳細な説明】
【優先権】
【０００１】
[0001]本特許出願は、本発明の譲受人に譲渡され、参考としてここに援用する２００３年１２月２３日に出願された「Flexible and Efficient Method for Limiting the Resource Usage ofComputer Programs」と題する対応するプロビジョナル特許出願第６０／５３２，３５９号に対する優先権を請求する。
【発明の分野】
【０００２】
[0002]本発明は、コンピュータプログラムをチェックする分野に係り、より詳細には、本発明は、コンピュータプログラムの動的チェックに関する情報を静的に検証するような静的及び動的の両チェックを遂行することに係る。
【発明の背景】
【０００３】
[0003]プログラムは、ここで、コードプロデューサと称される個人により生成されて、ここで、コードコンシューマーと称される個人により実行される。コードコンシューマーは、コードプロデューサにより生成された信頼性のないプログラムを実行することを希望しない。というのは、プログラムは、ファイルやネットワークのようなリソースにアクセスする機能を与えるランタイムライブラリーを経てコードコンシューマーのコンピュータと通信するからである。コードコンシューマーは、プログラムの安全性を確保することを希望し、これは、プログラムがユーザデータを破壊せず、又、プライベートデータを外部ソースへエクスポートせず、且つシステムリソースを悪用しないことを意味する。
【０００４】
[0004]コンピュータプログラムの安全性を確保するための既存の方法は多数ある。これらは、計算上の分離、動的チェック及び静的チェックを含む。計算上の分離については、安全性の問題に対する１つの解決策は、コンピューティング装置を分離し、新たなコード又は通信チャンネルを許さないことである。この解決策は、装置の有効性を制限するので、満足なものではない。
【０００５】
[0005]動的チェックは、各潜在的に非安全なオペレーションを、それが生じる直前にチェックするプロセスを指す。例えば、安全性ポリシーが特定のディレクトリーへのアクセスを禁止する場合には、ランタイム（ＲＴ）ライブラリー又はＲＴモニタが各ファイルアクセスをチェックしなければならない。動的チェックは、２つの利点を有する。第１に、正確である。即ち、プログラムが実際に犯そうとしている安全性違反しか検出しない。チェッカーが違反を検出する場合、ユーザがチェッカーをターンオフしていれば、プログラムが実際に違反を犯すことになる。第２に、簡単である。チェッカー全体は、適当なルーチンと共にランタイムライブラリーに課せられる簡単なチェックで構成される。しかしながら、動的チェックは、２つの基本的な欠点がある。第１に、考えられる最後の瞬間にエラーを検出するので、遅い。警報なしにプログラムを終了させると、ユーザが驚き又は混乱するか或いは貴重なデータを失わせることになるので、この遅さが問題である。又、プログラムを終了させるときには、プログラムが割り当てたオペレーティングシステム（ＯＳ）リソースを回復することが困難であり、他の実行中プログラムの性能に悪影響を及ぼすことがある。第２に、動的チェックは、非効率的である。各オペレーションは、その実行前にチェックを遂行するので、これらのチェックは、ＣＰＵ時間の著しい部分を占有する。
【０００６】
[0006]静的チェックでは、全プログラムがその実行前に分析され、それが安全であるかどうか調べる。静的チェックは、２つの利点がある。第１に、静的チェックは、実行を開始する前に全ての欠陥を検出するという点で、早い。従って、チェッカーがプログラムを検証する場合に、ランタイムエラーが生じることはなく、それ故、ユーザがデータを失うこともないし、ＯＳがプログラムを終了しなければならないこともない。第２に、静的チェックは、効率的である。全てのチェックは、プログラムテキストに基づいて行われ、従って、ランタイムチェックは何であれ行われず、プログラムは、完全に信頼性のあるプログラムと同じ速度で実行できる。又、静的チェックも、２つの欠点がある。第１に、静的チェックは、複雑なプログラムの振舞いに関して推論するよう試みるので、複雑である。第２に、静的チェックは、幾つかの安全性プログラムを拒絶するという意味で、不完全である。この不正確さは、２つの原因で生じる。第１に、プログラムが複雑である。チェッカーは、多数の簡単なプログラムを取り扱うことができるが、実際に関心のある多数のプログラムプロパティを決定できないので、検証できない安全性プログラムが幾つかある。第２に、静的なチェッカーは、プログラムは知っているがその入力を知らないという点で、不完全な情報で実行する。静的なチェックで得られる最良の結果は、ある入力が非安全なアクションを生じるかどうか決定することである。この入力が実際に生じるかどうか決定することができない。
【０００７】
[0007]リソース使用を制限する状況において、動的チェックとは、プログラムの実行中にリソースマネージャーがチェックを遂行するプロセスを指し、一方、静的チェックとは、プログラムの実行前にリソースマネージャーがチェックを遂行するプロセスを指す。動的チェックは、柔軟性があるが、非効率的であり、一方、静的チェックは、効率的であるが、柔軟性がない。
【発明の概要】
【０００８】
[0008]プログラムコードについてチェックを遂行するための方法及び装置。一実施形態において、この方法は、プログラムコードを受け取るステップと、そのプログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証するステップであって、前記プログラムコードにおける１つ以上の動的なチェックの各々が前記プログラムコードにおけるオペレーションをチェックするようなステップと、を備えている。
【０００９】
[0009]本発明は、その構造及び動作方法を含めて、添付図面に若干概略的に示されている。
【発明の詳細説明】
【００１０】
[0031]コンピュータプログラムをチェックするための方法及び装置について説明する。本発明は、動的なチェックが含まれたオペレーションを実行する前に、コンピュータプログラムにおいて動的なチェックを任意に移動することを許す。本発明の実施形態は、静的な情報を使用して、プログラムが充分な動的チェックを行うのを検証する。従って、本発明は、柔軟性があると共に効率的でもある。本発明は、静的及び動的の両チェッカーの利点を発揮する。動的チェッカーと同様に、４つ全部のプログラムを安全に実行することができる。静的なチェッカーと同様に、各プログラムにおいて得られる静的な情報を使用して、より効率的に実行することができる。一実施形態において、ここに述べる技術は、全ての逐次コンピュータプログラムに適用され、リソース制限を実施するＣＰＵの時間を、従来の方法より著しく僅かしか費やさない。
【００１１】
[0032]一実施形態において、この方法は、コンピュータプログラムにより使用されるリソースを制限するのに使用できる。リソースは、物理的リソース（例えば、ＣＰＵ、メモリ、ディスク、ネットワーク）、及び仮想リソース（例えば、ファイル、プロセス）の両方を含むことができる。一実施形態において、プログラムが許容以上のリソースを使用しようと試みる場合に、プログラムのシステムストップ実行で、割り込みを発生し、例外を生じさせ、等々により、リソースが制限される。
【００１２】
[0033]一実施形態において、リソースは、ユーザが定義したセキュリティポリシーに基づいて制限される。このポリシーは、各プログラムが使用できるリソースと、それに対応する使用限界とを指定する。一実施形態において、リソース使用制限は、リソースの使用量が、オペレーティングシステム又はシステムポリシーのいずれかにより規定された上限以内であることを保証する。これは、下限や、他の種類の制約、例えば、リソースの使用率の上限及び下限へも、容易に拡張できることに注意されたい。
【００１３】
[0034]一実施形態において、ここに述べるコード安全性に関する技術は、安全性に関するリソース予約を特定するための新規な抽象及び注釈(annotation)に基づいている。一実施形態において、この方法は、オペレーティングシステムからリソースを得る新規なクラスのインストラクション又はオペレーションに基づくものである。これらの新規なインストラクションで構築すると、一実施形態において、動的な（実行時間）コンポーネント、及び静的な（ロード時間又はコンパイル時間）コンポーネントが指示される。従って、本発明の実施形態は、混合即ちハイブリッド式解決策を使用する。動的なコンポーネントは、オペレーティングシステムからリソースを得てそれをオペレーティングシステムへ返送する１組の予約機能である。プログラムは、全てのリソースを使用する前にそれらを予約する場合には安全と考えられる。静的なコンポーネントは、プログラムが安全かどうかチェックするベリファイア(verifier)である。一実施形態において、ベリファイアは、ここに定義する最適なやり方でしか安全なプログラムを受け容れない。
【００１４】
[0035]リソース制限のための従来の方法は、リソース使用ごとに１つの予約を使用するので、非効率的である。本発明の実施形態は、多数のリソース使用に対して１つの予約を使用するので、何桁も効率の良いものとなる。
【００１５】
[0036]本発明の一実施形態は、リソース使用に向けられるが、本発明は、他の領域へと拡張されてもよく、例えば、データ破壊及びプライバシー違反に向けられてもよい。例えば、望ましい安全性プロパティは、プログラムがファイルを読み取ることができない場合に、そのファイルのデータをエクスポートできないことでよい。
【００１６】
[0037]以下、本発明をより完全に説明するために多数の細部について述べる。しかしながら、当業者であれば、本発明は、これら特定の細部を伴わずに実施できることが明らかであろう。換言すれば、良く知られた構造及び装置は、本発明を不明瞭にしないために、詳細に示すのではなく、ブロック図の形態で示す。
【００１７】
[0038]以下の詳細な説明のある部分は、コンピュータメモリ内のデータビットに対するオペレーションをアルゴリズム及び記号表示の形態で示す。これらアルゴリズム記述及び表示は、データ処理技術の当業者により、それらの仕事の実体をこの技術の他の当業者へ最も有効に伝えるために使用される手段である。アルゴリズムとは、ここでは、一般に、希望の結果を導くステップの自己矛盾のないシーケンスであると考えられる。これらステップは、物理的な量の物理的操作を要求する。通常、必ずしもそうでないが、これらの量は、記憶、転送、合成、比較、及びその他、操作することのできる電気的又は磁気的信号の形態をとる。時には、主として、共通の使用という理由で、これらの信号を、ビット、値、エレメント、記号、キャラクタ、項、数字等として参照するのが便利であると分かっている。
【００１８】
[0039]しかしながら、これら及び同様の用語は、全て、適当な物理的量に関連されるべきで、且つこれらの量に適用される便利なラベルに過ぎないことを銘記されたい。特に指示のない限り、以下の説明から明らかなように、この説明全体にわたり、「処理」又は「コンピューティング」又は「計算」又は「決定」又は「表示」等の用語を使用する検討は、コンピュータシステム又は同様の電子的コンピューティング装置のアクション及び処理であって、コンピュータシステムのレジスタ及びメモリ内の物理的（電子的）量として表わされたデータを、コンピュータシステムのメモリ又はレジスタ、或いは他のこのような情報記憶、送信又は表示装置内の物理的量として同様に表わされる他のデータへと操作及び変換するものを指すことが明らかであろう。
【００１９】
[0040]又、本発明は、ここに述べるオペレーションを実行するための装置にも係る。この装置は、要求される目的に対して特別に構成されてもよいし、或いはコンピュータに記憶されるコンピュータプログラムにより選択的にアクチベートされ又はコンフィギュレーションされる汎用コンピュータを備えてもよい。このようなコンピュータプログラムは、コンピュータ読み取り可能な記憶媒体、例えば、これに限定されないが、フロッピーディスク、光学ディスク、ＣＤ−ＲＯＭ、及び磁気−光学ディスクを含む任意の形式のディスク、リードオンリメモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、ＥＰＲＯＭ、ＥＥＰＲＯＭ、磁気又は光学カード、或いは電子的インストラクションを記憶するのに適していて、コンピュータシステムバスに各々結合される任意の形式の媒体に記憶されてもよい。
【００２０】
[0041]ここに述べるアルゴリズム及びディスプレイは、特定のコンピュータ又は他の装置に固有に関連したものではない。種々の汎用システムが、ここに述べる教示に基づくプログラムと共に使用されてもよいし、又は必要な方法ステップを実行するために更に特殊な装置を構成するのに便利であると分かった。種々のこれらシステムに必要な構造は、以下の説明から明らかであろう。更に、本発明は、特定のプログラミング言語を参照して説明しない。ここに述べる本発明の教示を実施するのに種々のプログラミング言語を使用できることが明らかであろう。
【００２１】
[0042]マシン読み取り可能な媒体は、マシン（例えば、コンピュータ）で読み取り可能な形態で情報を記憶し又は送信するためのメカニズムを含む。例えば、マシン読み取り可能な媒体は、リードオンリメモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、磁気ディスク記憶媒体、光学記憶媒体、フラッシュメモリ装置、電気的、光学的、音響的又は他の形態の伝播信号（例えば、搬送波、赤外線信号、デジタル信号等）、等々を含む。
【００２２】
[0043]図１は、プログラムコードをチェックするためのプロセスの一実施形態を示すフローチャートである。このプロセスは、ハードウェア（例えば、回路、専用ロジック等）、ソフトウェア（汎用コンピュータシステム又は専用マシンにおいて実行されるような）、或いはその両方の組合せを含んでもよい処理ロジックにより実行される。
【００２３】
[0044]図１を参照すれば、このプロセスは、少なくとも１つの静的なチェックと、動的チェックのための少なくとも１つの動的なチェックとの組合せを処理ロジックが選択することで開始される（処理ロジック１０１）。一実施形態において、静的チェックは、注釈の形態の抽象を含み、この注釈は、これが追加されるプログラムに対して動的なコストをもたない（例えば、プログラムが実行されるときにクロックサイクルを消費するオペレーションではない）。一実施形態において、静的なチェックは、当該リソースを消費するマシンインストラクションを抽象的に表わす。
【００２４】
[0045]一実施形態において、１つ以上の動的なチェックは、リソース予約を特定するためにプログラムに追加できる１つ以上の動的な注釈を含む。静的なチェックとは異なり、動的なチェックは、プログラムに追加されたときに、そのプログラム実行時に実行すべき１つ以上のサイクルを被るオペレーションを備えている。一実施形態において、１つ以上の動的なチェックのうちの少なくとも１つは、リソースの使用をチェックするためのものである。上述したように、リソースは、物理的なリソース（例えば、実行される多数の中央処理ユニット（ＣＰＵ）インストラクション、メモリスペース、ディスクスペース、及びネットワーク帯域巾）でもよいし、或いは仮想リソース（例えば、ファイル取り扱い、プロセス）でもよい。
【００２５】
[0046]もちろん、オペレーティングシステムは、最終的に、全てのリソースを仮想化する。一実施形態において、現在使用、累積使用、及び使用率を含む多数のリソース使用プロパティが実施される。
【００２６】
[0047]次いで、処理ロジックは、静的及び動的チェックを表すことに関する注釈をプログラムコードに追加する（処理ブロック１０２）。一実施形態において、１つ以上の注釈のうちの少なくとも１つは、プログラムコードの一部分により使用するためのリソースを予約するオペレーションを含む。
【００２７】
[0048]プログラムに注釈が付けられた後に、処理ロジックは、プログラムコードを受け取る（処理ブロック１０３）。
【００２８】
[0049]次いで、処理ロジックは、プログラムコードにおける１つ以上の動的チェックに関する情報を静的に検証し、ここで、プログラムコードにおける１つ以上の動的チェックの各々は、プログラムコードにおけるオペレーションをチェックするためのものである（処理ブロック１０４）。動的チェックの少なくとも１つは、オペレーションが非安全であるかどうか決定することができる。一実施形態において、処理ロジックは、１つ以上の動的チェックの静的分析を遂行することによりプログラムコードにおける１つ以上の動的チェックに関する情報を静的に検証する。
【００２９】
[0050]一実施形態において、プログラムコードにおける１つ以上の動的チェックに関する情報を静的に検証することは、リソースを予約するためのプログラムコードにおけるオペレーションを静的にチェックして、オペレーションにより予約されているリソースが、プログラムコードにおいてリソースを消費する全ランタイムオペレーションを考慮するに充分なものかどうか決定することを含む。
【００３０】
[0051]一実施形態において、処理ロジックは、プログラムコードが、ランタイム中に１つ以上のリソースのうち、プログラムコードが実行前に予約したものより多くを使用しようとするかどうかチェックすることにより、１つ以上の動的チェックに関する情報を静的に検証する。
【００３１】
[0052]一実施形態において、処理ロジックは、ランタイム中に動的チェックを呼び出すことによりプログラムコードの動的チェックを遂行する（処理ブロック１０５）。
【００３２】
[0053]一実施形態において、プロセスは、更に、処理ロジックがプログラムコードによるリソース使用を制限することを含む（処理ブロック１０６）。これは、リソース使用が限界を越えているという決定に応答して行われる。一実施形態において、プログラムコードによるリソース使用を制限することは、プログラムコードの実行を停止することを含む。別の実施形態において、処理ロジックは、例外を引き起こしてもよいし、又はリソース使用が限界を越えているという決定に応答して割り込みを発生してもよい。
【００３３】
[0054]本発明の実施形態は、新たなクラスのランタイムオペレーション「ａｃｑｕｉｒｅ（取得）」及び新たなクラスの注釈「ｃｏｎｓｕｍｅ（消費）」に対して抽象を使用する。ａｃｑｕｉｒｅオペレーションは、予約インストラクションの一例であり、コードプロデューサにより生成されたプログラムにおいて生じる。一実施形態において、ｃｏｎｓｕｍｅ注釈は、コードコンシューマーのランタイムライブラリーにおいて生じる。
【００３４】
[0055]オペレーションａｃｑｕｉｒｅ  ｎは、プログラムがｎ個のリソースユニットを使用できるかどうか調べるための動的チェックを遂行するのに使用される。一実施形態において、もしそうでなければ、プログラムを中断することができる。ａｃｑｕｉｒｅオペレーションがブール値を返送するか又はユーザ取り扱い可能な例外を引き起こすような変形例も考えられる。リソースが使用可能である場合には、それらを、プログラムが後で使用するようにマークし、従って、他のプログラムはそれらを取得できない。
【００３５】
[0056]注釈ｃｏｎｓｕｍｅ  ｎは、リソースを消費する全てのランタイムオペレーションをマークする。一実施形態では、動的チェックを遂行せず、従って、ランタイムコストをもたない。しかしながら、コードコンシューマーは、プログラムが全てのコンシューマーを考慮するに充分なリソースを取得することを静的にチェックする。従って、このようなケースでは、注釈ｃｏｎｓｕｍｅは、リソース消費オペレーションに対する抽象である。
【００３６】
[0057]一実施形態において、上述した注釈、静的及び動的、に対する引数ｎの値は、正である。これは、プログラム実行の前に、静的にチェックすることができる。図２は、予約が追加された４つのプログラムを示す。図２を参照すれば、プログラム「動的」は、各リソースを、使用の直前に予約する。プログラム「静的」及び「混合１」は、全てのリソースを始めに予約する。プログラム「混合２」は、あるリソースを、その外側ループをめぐるたびに予約する。静的チェッカーとは異なり、ここに述べる技術は、４つのプログラムを全部取り扱う。動的チェッカーとは異なり、この解決策は、各プログラムに存在する静的情報を使用して、より効率的に実行すると共に、動的チェックが安全確保に充分であることを保証する。
【００３７】
[0058]従って、本発明の一実施形態は、オリジナルのリソース使用問題（ｃｏｎｓｕｍｅ≦ｑｕｏｔａ）の中点を識別し、これは、チェックを２つのフェーズに仕切り、各フェーズに対して静的又は動的チェックの最も適した組合せを選択するのを許すものである。
【００３８】
[0059]図３は、コードコンシューマーのセキュリティポリシーによりプログラムに割り当てられた全てのリソースを最初に含む単一のリソースプールを備えた典型的な動的リソースチェッカーを示す。ランタイムライブラリーオペレーションは、リソースを消費するときにそれらをプールから除去する。オペレーションがリソースを必要とするが、プールが空である場合には、プログラムを終了する。
【００３９】
[0060]図４は、望ましいプールリソースモデルを示す。図４を参照すれば、プログラムは、それがリソースを使用する前にそれらリソースを予約する。付加的なａｃｑｕｉｒｅオペレーション（注釈）のために、２プールモデルは、１プールモデルより高価に見えるが、そうではない。というのは、ａｃｑｕｉｒｅオペレーション（注釈）は動的であり、一方、ｃｏｎｓｕｍｅ注釈は静的であるからである。従って、ｃｏｎｓｕｍｅ注釈は、実行時間を全く必要としない。更に、ａｃｑｕｉｒｅオペレーションは、一度に多数のリソースをプログラム使用へ転送するので、ａｃｑｕｉｒｅオペレーションは、ｃｏｎｓｕｍｅ注釈より遥かに少ない。従って、２プールモデルにおけるａｃｑｕｉｒｅオペレーション及びｃｏｎｓｕｍｅ注釈は、１プールモデルにおけるｃｏｎｓｕｍｅ注釈よりも非常に短い時間しか必要としない。
【００４０】
[0061]メモリ又はファイル記述子のようなあるリソースは、割り当て、解放し、次いで、再び割り当てることができる。これらのリソースは、更新可能又は再使用可能と称される。リソースが再び使用できることを指示するために、これらリソースに対するｒｅｌｅａｓｅ（解除）オペレーション（動的な注釈）がリサイクル１で注釈付けされる。更に、充分なリソースが「未使用」とされた後に、ｒｅｌｅａｓｅ  ｎオペレーションを遂行して、これらリソースをリソースモニタへ解除して戻すことができる。このオペレーションは、プログラムの異なるセクションにおいてリソースの予約を再び可能にするか、又はそれらを他のプログラムに使用するのを可能にする。
【００４１】
セキュリティポリシーアプリケーション
[0062]一実施形態において、コードコンシューマーは、３つの部分、即ち１組のリソースと、１組の（任意の）リソース限界と、リソース及びオペレーション使用の記述とを含むセキュリティポリシーを定義する。
【００４２】
[0063]リソース限界は、任意のもので、この場合、対応するリソースは、限界定めされていない。アノテーター(annotator)及びベリファイアは、限界定めされていないリソースを無視するように選択できる。即ち、アノテーターは、それらに対して予約を挿入する必要がなく、そしてベリファイアは、それらを追跡する必要がない。それ故、コードコンシューマーではなく、コードプロデューサが予約を追加する場合には、コードコンシューマーのセキュリティポリシーをダウンロードして、予約する必要がないのはどのリソースか分かるようにするのが便利である。コードプロデューサが必要以上に予約を挿入する場合に、コードは依然検証をパスするが、必要に満たない速度で実行する。
【００４３】
[0064]ここに述べる技術により実施できるセキュリティポリシーは、例えば、次のものを含む。
−装置においてプログラムによりオープンできるウインドウの最大数は、５である。
−装置においてプログラムがオープンできるソケットの最大数は、２である。
−装置においてプログラムが書き込みできるメモリの最大量は、１０ＫＢである。
特定の値は、任意であることに注意されたい。
【００４４】
アーキテクチャー及びプロトコル
[0065]図５は、予約による抽象的リソース使用安全性を示す。図５を参照すれば、ｃｏｎｓｕｍｅがｑｕｏｔａ（割当量）以下であるよう保証することは、予約により実施できる。本発明の実施形態における基本的なコンポーネントは、２つの式、ｃｏｎｓｕｍｅ≦ａｃｑｕｉｒｅ及びａｃｑｕｉｒｅ≦ｑｕｏｔａを実施する。一実施形態において、第１の式は、静的にチェックされ、第２の式は、動的にチェックされる。図６は、コード安全性を静的及び動的コンポーネントに仕切るところを示す。図６を参照すれば、コード６００は、最初、コンパイラー６０１により条件ｃｏｎｓｕｍｅ≦ａｃｑｕｉｒｅに対して静的にチェックされ、次いで、ａｃｑｕｉｒｅ≦ｑｕｏｔａを動的に保証するマシン６０３において実行される。
【００４５】
[0066]一実施形態において、予約インストラクション（動的注釈）は、ａｃｑｕｉｒｅ及びｒｅｌｅａｓｅであり、これらは、各々、リソースを動的に要求しそしてオペレーティングシステムへ返送する。一実施形態において、注釈は、ｃｏｎｓｕｍｅ及びｒｅｃｙｃｌｅと命名され、これらは、静的なプール（図４を参照）において動作し、ランタイムコストを被らない。
【００４６】
[0067]静的なチェック手順を説明するために、整数値で計算する簡単な必須のプログラミング言語が使用されてもよい。以下、この手順は、ある任意の単位でその量が測定される１つの当該リソースのみを使用して説明する。注釈ｃｏｎｓｕｍｅ  ｅは、ｅ個のリソース単位を使用するオペレーションをモデリングするのに使用され、ここで、ｅは言語での表現である。コマンドａｃｑｕｉｒｅ  ｅは、オペレーティングシステムからｅ個のリソース単位を予約する。このコマンドは、失敗となるかもしれないが、もし成功した場合には、実行中のプログラムに対してｅ個のリソース単位が予約されたことが分かる。リソースをオペレーティングシステム及び静的プールへ各々返送する対応コマンド及び注釈は、各々、ｒｅｌｅａｓｅ及びｒｅｃｙｃｌｅと称される。説明上、予約されたがまだ使用されていないリソースは、ここでは、「入手可能な(available)」リソースと称される。
【００４７】
[0068]図７は、標準的なバッカス記法(Backus-Naurformat)で言語の一実施形態の完全な定義を示す。一実施形態において、変数ｘは、整数値しかとらない。式ｃｏｎｄ（ｂ、ｅ１、ｅ２）は、ブール式ｂの値が真である場合は、値ｅ１を有し、さもなければ、値ｅ２を有する。同様に、コマンドｃｏｎｄ（ｂ、Ｐ１、Ｐ２）は、ｂの値が真である場合はコマンドＰ１に等しく、さもなければ、コマンドＰ２に等しい。命題結合記号∧、∀、⇒は、それらの通常の意味を有する。
【００４８】
[0069]ａｃｑｕｉｒｅ、ｒｅｌｅａｓｅ、ｃｏｎｓｕｍｅ及びｒｅｃｙｃｌｅ注釈に加えて、一実施形態では、コマンドａｖａｉｌａｂｌｅ（Ａ、ｅ）が使用される。このコマンドは、実行中に無視されるが、チェック手順に対する仕様として働く。プログラマーは、このコマンドを使用して、所与のポイントでＡが真であり且つ少なくともｅ個のリソース単位が予約されたがまだ使用されていないことを主張する。この主張は、チェック手順の一部分として静的にチェックされる。
【００４９】
[0070]ループコマンドは、不変量（Ａ、ｅ）で注釈が付けられることにも注意されたい。静的なチェック中に、述部Ａは、それが保持され且つループコマンドの実行前に少なくともｅ個のリソース単位が入手可能であるかどうか決定するために検証される。静的チェッカーのタスクを簡単にするために、不変量は、ブール式の連結に制約され、そして含意の左側は、単に述部へと制約される。
【００５０】
[0071]より詳細には、式及びコマンドの意味は、以下の通りであり、又、実行が失敗に至る正確な道筋は、プログラミング言語構造のオペレーション仕様に対する良く知られた解決策に従い明確にされる。例えば、ここで使用する標準的な表記法の更なる説明については、Ｊ．Ｃ．ミッチェル著のFoundations for Programming Language、ＭＩＴプレス、１９９６年、を参照されたい。実行状態は、可変の名前を整数値にマップする環境σと、入手可能なリソースの量を表わす自然数ｎとの対＜σ、ｎ＞である。式[[ｅ]]σは、環境σにおける整数式ｅの値に対して書き表され、そして[[ｂ]]σは、環境σにおけるブール式ｂの値に対して書き表される。例えば、次のようになる。
[[ｅ１]]σ、 [[ｂ]]σ＝真の場合
[[ｃｏｎｄ（ｂ、ｅ１、ｅ２）]]σ＝｛
[[ｅ２]]σ、 [[ｂ]]σ＝偽の場合
【００５１】
[0072]定義の他のケースは、簡単である。表記法σ［ｘ：＝ｎ］は、ｘがｎにセットされることを除いてσに等しい環境を示す。
【００５２】
[0073]ここに述べる言語に使用するための基本的なビルディングブロックは、安全条件ジェネレータである。一実施形態において、この安全条件ジェネレータは、プルーフチェッカーと結合されて、ベリファイアを形成する。このベリファイアは、プログラムが全てのｃｏｎｓｕｍｅ注釈を網羅するに充分なａｃｑｕｉｒｅオペレーションを有することをチェックし、従って、プログラムが、予約したもの以上のリソースを使用しないことを指示する。一実施形態において、ベリファイアは、ｒｅｌｅａｓｅ及びｒｅｃｙｃｌｅオペレーションにより解放されたリソースも考慮に入れる。
【００５３】
[0074]一実施形態において、ベリファイアは、コードコンシューマーの信頼されるコンピューティングベース（ＴＣＢ）の一部分である。  これは、コードコンシューマーにおいてリソース使用安全性を確保するためにプロデューサのコードが満足しなければならない最も弱い条件を発生するという点で、考えられる最も一般的なベリファイアである。従って、これは、プロデューサのコードを注釈付けするのに使用されるメソッドに対して寛容でもある。
【００５４】
[0075]ベリファイアは、ソースコード又はバイナリーコードを入力として各々取り入れできるように、ソース及びバイナリーの両フォームで形成することができる。ここでは、ソースコードフォームがチェックされるが、バイナリーフォームも形成が容易である。一実施形態において、コードプロデューサは、コードコンシューマーにバイナリーコードしか送信しない。
【００５５】
[0076]信頼性のあるベリファイアは、コード注釈付け及びプロダクションプロセスに多数の仕方で一体化することができる。コード注釈付けは、コードコンシューマー又はコードプロデューサ或いはおそらくその両方により遂行することができる。又、注釈付けの結果は、いずれかの当事者により手動で編集することもできる。これが可能であるのは、ベリファイアが、使用する注釈付け方法の選択とは独立しているからである。
【００５６】
[0077]図８は、注釈付けを（コードプロダクションと共に）遂行するコードプロデューサと、検証を（実行と共に）遂行するコンシューマーとを示す。この場合に、コードプロデューサは、ソースアノテーターを実行し、そしてコードコンシューマーは、バイナリーベリファイアを実行する。一実施形態において、ベリファイアは、ＴＣＢの一部分であるが、アノテーターは、そうではない。この分離は、コードプロデューサが、おそらく、自動的アノテーター挿入より少数の予約を使用することで、コードを改善するのを許す。ベリファイアは、保証を与え、一方、注釈付けプロセスは、効率について最適化することができる。
【００５７】
[0078]プロデューサとベリファイアとの間の基本的コンポーネントの別の考えられる分離が、図９に示されている。図９を参照すれば、コンシューマーは、コードに注釈付けし、バイナリーベリファイアを実行する。ベリファイアは、ＴＣＢの一部分であり、アノテーターは、あってもなくてもよい。
【００５８】
[0079]図８及び９において、別の実施形態では、コンシューマーは、汎用コンピュータシステム、専用マシン、移動装置（例えば、セルラー又は他のポータブル電話）等を備えてもよい。
【００５９】
ベリファイアの実施例
[0080]図１０は、ベリファイアの一実施形態のブロック図である。図１０を参照すれば、ベリファイア１０００は、プログラムの安全条件（ＳＣ）を計算する安全条件ジェネレータ１００１と、ＳＣを実際に立証するプローバー１００２とを備えている。
【００６０】
2007516538.tif 000002
【００６１】
[0082]結果Ｒは、次の形式の値の１つである。コマンドが通常に終了する場合には、Ｒは、新たな状態＜σ’、ｎ’＞となる。予約要求が失敗となった場合には、Ｒは、エラーＲｅｓｅｒｖａｔｉｏｎＦａｉｌｅｄ又はエラーＲｅｌｅａｓｅＦａｉｌｅｄとなる。プログラムが、入手可能以上のリソースを使用しようと試みる場合に、Ｒは、エラーＱｕｏｔａＥｘｃｅｅｄｅｄとなる。プログラムが特定の注釈を満足しない場合には、Ｒは、エラーＩｎｖＦａｉｌｕｒｅとなる。安全性プロパティは、ＱｕｏｔａＥｘｃｅｅｄｅｄ及びＩｎｖＦａｉｌｕｒｅエラーが生じないことを厳密に指定する。
【００６２】
[0083]図１１、１２及び１３は、各々、シーケンシング及び指定、条件及びループ、並びに予約のためのオペレーションセマンティックを示す。
【００６３】
[0084]又、オペレーションセマンティックスは、プログラムが、それに付随する注釈を満足し、さもなければ、エラーＩｎｖＦａｉｌｕｒｅを生じさせるよう確保することに注意されたい。安全プログラムは、ＩｎｖＦａｉｌｕｒｅ例外を決して引き起こさないので、これら付加的なルールに対するランタイムオーバーヘッドはない。ｃｏｎｓｕｍｅ（ｒｅｌｅａｓｅ）コマンドは、充分なリソースを入手できる場合に、幾つかの入手可能なリソースの消費（解除）を通常に終了させるか、或いはＱｕｏｔａＥｘｃｅｅｄｅｄエラーを発生するかのいずれかである。一実施形態において、ｃｏｎｓｕｍｅコマンドは、リソースについてのチェックを遂行しない。ａｃｑｕｉｒｅコマンドは、入手可能なリソースの量を増加するか、又はＲｅｓｅｒｖａｔｉｏｎＦａｉｌｅｄエラーを発生するかのいずれかである。この公式化において、ａｃｑｕｉｒｅコマンドは、非決定論的であると仮定する。実際に、その振舞いは、オペレーティングシステムにより決定される。ｒｅｃｙｃｌｅコマンドは、ある量の以前に使用されたリソースを静的なプールへ解除する。
【００６４】
2007516538.tif 000003
【００６５】
[0086]健全さについては、コマンドｃが与えられると、式（Ｐ’、ｅ’）＝ｓｃｇ（ｃ、（真、０））が計算される。状態＜σ、ｎ＞においてプログラムを実行するのが安全であることをチェックするために、式σ｜＝Ｐ’∧ｅ’≦ｎが検証される。この条件は、コマンドｃが状態σにおいて入手可能なｎ個のリソース単位で実行されるようにして実行する場合に、ｃがリソースを使い果たさないことを保証する。ｃが実際にリソースを使用する場合には、使用前にそれらを予約する。以下に述べるように、この検証手順は、健全である。
【００６６】
[0087]式σ｜＝Ｐは、述部Ｐが状態σに保持されることを指示する。Ｐは、状態σにより値が与えられる変数に対する述部で、これは、この技術で良く知られたように、式σ｜＝Ｐが命題結合記号に対して帰納法で定義されるのを許すことを想起されたい。主たる健全さの補題は、次のように表わされる。
【００６７】
2007516538.tif 000004
【００６８】
[0088]本質的に、この補題は、安全性ポリシーにより要求されるように、ＱｕｏｔａＥｘｃｅｅｄｅｄ及びＩｎｖＦａｉｌｕｒｅエラーが決して生じないことを保証する。
【００６９】
2007516538.tif 000005
【００７０】
[0090]従って、安全性が公式に定義され、これは、安全条件ジェネレータが健全であることを示す。即ち、安全条件が保持される場合に、プログラムは安全である。
【００７１】
[0091]一実施形態において、安全条件ジェネレータは、最適でもある。より詳細には、コマンドｃ及び状態＜σ、ｎ＞に対する安全条件は、コマンドｃが、状態σにおいて、入手可能なｎ個のリソース単位で実行される場合に、ｃがリソースを使い果たさないことを保証する。以下に示すように、安全条件ジェネレータは、以下に定義する全ての安全前提条件の中で論理的に最も弱いと考えられる条件を与えるという点で最適である。
【００７２】
2007516538.tif 000006
【００７３】
[0094]補題２  全てのコマンドｃ及びリソース−状態述部（Ｐ、ｅ）に対して、ｓｃｇ（ｃ、（Ｐ、ｅ））は、ｃ及び述部（Ｐ、ｅ）のための最も弱い前提条件である。
【００７４】
[0095]従って、この安全条件ジェネレータは、その発生される安全条件が、注釈を満足し且つリソース使用安全である全てのプログラムを捕獲するという点で、最適である。
【００７５】
安全条件ジェネレータ
[0096]一実施形態において、ベリファイアは、Ｄｉｊｋｓｔｒａの最も弱い前提条件計算法の変形を使用する。（Edsger Dijkstra、A Discipline of Programming、Prentice-Hall、１９７６年。）プログラムポイントごとに、不変量（Ａ、ｅ）が計算され、全ての実行において、そのポイントで、Ａが満足され、そして少なくともｅ個のリソース単位が入手可能となるようにする。一実施形態において、これらの不変量は、プログラム実行の終了に保持される不変量からスタートして計算される。
【００７６】
[0097]図１４は、安全条件ジェネレータ（ｓｃｇ）に対するコードの一実施形態であり、図１５は、安全条件ジェネレータ（ｓｃｇ）の一実施形態のオペレーションを示すフローチャートである。ここに述べる多数のケースにおいて、機能は、コード及びフローチャートの両フォームで表わされる。全てのケースにおいて、２つのフォームは完全に同等である。機能ｓｃｇ（ｃ、（Ｐ、ｅ））は、ｃの終りに保持される不変量（Ｐ、ｅ）を、ｃの始めに保持される不変量（Ｐ’、ｅ’）へマップする。ｓｃｇは、コマンドのシンタックスの反復により定義される。図１５及び１７のフローチャートでは、∀ｘがｆａ（ｘ）により表わされる。
【００７７】
プローバーの実施例
[0098]一実施形態において、安全条件ジェネレータは、プルーフコンストラクターと結合されて、プローバーを形成する。プローバーは、安全条件を立証するのに使用される。一実施形態において、述部に対する文法は、含意の左側を、完全な述部ではなく、注釈へと制約する。注釈は、ブール式の連結であり、そしてブール式は、整数式間の等式又は不等式である。
【００７８】
[0099]定義は、この制約を尊重する。一実施形態において、含意の左側の全ての式は、ループの不変量、前提及び事後条件、利用可能な条項から生じる。
【００７９】
[00100]従って、簡単な定理プローバーは、Ａ⇒Ｐが有効な場合及びその場合にのみｐｒｏｖｅ（Ａ、Ｐ）が当てはまるところでａｘｐ→ブールが使用されることを立証する。有効とは、普遍的な定量化のためのルールにより導入される定数及び全体的な変数の全ての値に対して式が真であることを意味する。最初に、一実施形態において、各機能ｆｓ安全条件ＳＣｆを立証するためにｐｒｏｖｅ（ｔｒｕｅ、ＳＣｆ）へのコールがなされる。図１６は、プローバーのコードの一実施形態であり、一方、図１７は、プローバーを示す等価フローチャートである。
【００８０】
[00101]Ａ⇒Ｐを立証するために、ｐｒｏｖｅは、ブール式ｂに到達するまでＰを繰り返しデコンポーズする。次いで、満足手順ｓａｔを使用してＡ⇒ｂが有効であるかどうかチェックする。通常そうであるように、Ａ⇒ｂは、その否定がＡ∧¬ｂが満足できない場合及びその場合にのみ有効である。従って、式ｓａｔは、（おそらく否定された）ブール式の連結においてコールされる。ｐｒｏｖｅは、可逆ルールを使用してＰをデコンポーズするので、これは、ｓａｔが健全で且つ完全である場合及びその場合にのみ、健全で且つ完全である。
【００８１】
[00102]満足手順の選択は、ブール式のフォームに依存する。ｃを定数とし、ｘ及びｙを変数又は非解釈項とすれば、不等式のフォームがｘ≧ｙ＋ｃ又はｘ≧ｃである場合に、ループの残余をベースとするアルゴリズムを使用することができる（Ｔ．Ｈ．コーメン、Ｃ．Ｅ．レイサーソン、及びＲ．Ｌ．リベスト著のAn Introduction to Algorithms、ザ・ＭＩＴプレス、１９９８年、第５３９ページ）。ショスタックは、このアルゴリズムを任意の不等式へと一般化している（ロバート・ショスタック著、Deciding Linear Inequalities by Computing Loop Residue、ジャーナル・オブ・ザ・ＡＣＭ、２８（４）：７６９−７７９、１９８１年１０月）。他の著名なアルゴリズムは、Ｓｕｐ−Ｉｎｆ（Ｗ．Ｗ．ブレッドソー著、The sup-Inf Method in Presurger Arithmetic, Technical Report、ユニバーシティ・オブ・テキサス・マス・デパートメント、１９７４年１２月）、及びＳｉｍｐｌｅｘである。
【００８２】
[00103]ブール式が、加算、減算、及び定数乗算以外の関数を含む場合には、それらを非解釈のままにする。即ち、任意の１組の関数に対して健全な推論のみがなされる。即ち、これらの関数は、等しい引数を等しい結果にマップするものであり、ｓａｔ及びｐｒｏｖｅは、このような全ての推論を行うので、このシステムに対しても完全であることだけを仮定する。しかしながら、プログラムに使用される特定の関数については、それらは、不完全である。この制限のために、プログラマーは、注釈を、ｓａｔが取り扱いできるフォームに限定することを希望してもよい。
【００８３】
[00104]一次不等式及び非解釈関数を取り扱う著名な満足手順は、２つある。その一方は、ネルソン及びオッペンによるもので（グレッグ・ネルソン著、Techniques for Program Verification、Technical Report CSL-81-10、Xerox Palo Alto ResearchCenter、１９８１年）、スタンフォード・パスカル・ベリファイア（デビッド・ラッカム氏等著、Stanford Pascal Verifier User Manual、Technical Report STAN-CS-79-731、Department of ComputerScience、StanfordUniversity、１９７９年３月）、及びエクステンデッド・スタティック・チェッカー（グレッグ・ネルソン著、Techniques for Program Verification、Technical Report CSL-81-10、Xerox Palo Alto ResearchCenter、１９８１年）(デビット・デトレフ著、An Overview ofthe Extended Static Checking System, In Proceedings of the First Formal Methodsin Software Practice Workshop、１９９６年）（デビッドＬ．デトレフ氏等著、Extended Static Checking、SRC Research Report 159、Compaq Systems Research center、130 Lytton Avenue、 Palo Alto、１９９８年１２月）により実施されている。その他方は、ショスタックによるもので（ロバートＥ．ショスタック著、Deciding Combinations of Theories、Journal of the ACM、３１（１）：１−１２、１９８４年１月）、プロートタイプベリフィケーションシステム（ＰＶＳ）（Ｓ．オウア氏等著、PVS: A Prototype Verification System, In Deepak Kapur, editor, 11thInternational Conference on Automated Deduction (CADE), volume 607 of LectureNotes in Artificial Intelligence、第７４８−７５２ページ、サラトガ、ニューヨーク、１９９２年６月、スプリンガー−ベルラグ）において実施されている。
【００８４】
[00105]図１８は、ｗｈｉｌｅコマンドで書かれた小さなループを示す。この場合に、プログラマーは、手で不変量をループに注釈付けする。図１９は、この実施例に対する安全条件を示す。これを導出するために、式ｓｃｇ（ｃ、真、０）が計算される。ある簡単化の後に、この安全条件が有効であることが示される。
【００８５】
移動電話の実施例
[00106]図２０は、セルラー電話の一実施形態のブロック図である。
【００８６】
[00107]図２０を参照すれば、セルラー電話２０１０は、アンテナ２０１１と、高周波トランシーバ（ＲＦユニット）２０１２と、モデム２０１３と、信号処理ユニット２０１４と、制御ユニット２０１５と、外部インターフェイスユニット（外部Ｉ／Ｆ）２０１６と、スピーカ（ＳＰ）２０１７と、マイクロホン（ＭＩＣ）２０１８と、ディスプレイユニット２０１９と、操作ユニット２０２０と、メモリ２０２１とを備えている。
【００８７】
[00108]外部ターミナル２０３０は、外部インターフェイス（外部Ｉ／Ｆ）２０３１と、ＣＰＵ（中央処理ユニット）２０３２と、ディスプレイユニット２０３３と、キーボード２０３４と、メモリ２０３５と、ハードディスク２０３６と、ＣＤ−ＲＯＭドライブ２０３７とを備えている。
【００８８】
[00109]セルラー電話２０１０のメモリ（例えば、メモリ２０２１、メモリ２０３５、及びハードディスク２０３６）と協働するＣＰＵ２０３２は、上述したオペレーションを遂行するように協働する。
【００８９】
コンピュータシステムの実施例
[00110]図２１は、ここに述べるオペレーションの１つ以上を遂行できるコンピュータシステムの実施例のブロック図である。これらブロック又はこれらブロックのサブセットは、ここに述べる技術を遂行するために、例えば、セルラー電話のような装置に一体化できることに注意されたい。
【００９０】
[00111]図２１を参照すれば、コンピュータシステム２１００は、クライアント又はサーバーコンピュータシステムの一実施例を構成してもよい。コンピュータシステム２１００は、情報を通信するための通信メカニズム又はバス２１１１と、情報を処理するためにバス２１１１に結合されたプロセッサ２１１２とを備えている。プロセッサ２１１２は、例えば、ＰｅｎｔｉｕｍＴＭ、ＰｏｗｅｒＰＣＴＭ、ＡｌｐｈａＴＭ等のマイクロプロセッサを含むが、これに限定されるものではない。
【００９１】
[00112]システム２１００は、更に、プロセッサ２１１２により実行されるべき情報及びインストラクションを記憶するためにバス２１１１に結合されたランダムアクセスメモリ（ＲＡＭ）又は他の動的記憶装置２１０４（メインメモリと称される）を備えている。又、メインメモリ２１０４は、プロセッサ２１１２によるインストラクションの実行中に一時的変数又は他の中間情報を記憶するのに使用されてもよい。
【００９２】
[00113]又、コンピュータシステム２１００は、プロセッサ２１１２のための静的情報及びインストラクションを記憶するためにバス２１１１に結合されたリードオンリメモリ（ＲＯＭ）及び／又は他の静的記憶装置２１０６と、磁気ディスク又は光学ディスク及びそれに対応するディスクドライブのようなデータ記憶装置２１０７とを備えている。このデータ記憶装置２１０７は、情報及びインストラクションを記憶するためにバス２１１１に結合される。
【００９３】
[00114]コンピュータシステム２１００は、更に、コンピュータユーザに情報を表示するためにバス２１１１に結合された陰極線管（ＣＲＴ）又は液晶ディスプレイ（ＬＣＤ）のようなディスプレイ装置２１２１に接続することもできる。又、プロセッサ２１１２へ情報及びコマンド選択を通信するために、アルファニューメリック及び他のキーを含むアルファニューメリック入力装置２１２２をバス２１１１に結合してもよい。付加的なユーザ入力装置は、プロセッサ２１１２に方向情報及びコマンド選択を通信すると共に、ディスプレイ２１２１上のカーソル移動を制御するために、バス２１１１に結合されたマウス、トラックボール、トラックパッド、スタイラス、又はカーソル方向キーのようなカーソル制御器２１２３である。
【００９４】
[00115]バス２１１１に結合できる別の装置は、ペーパー、フィルム等の媒体、又は同様の形式の媒体にインストラクション、データ、又は他の情報を印刷するのに使用できるハードコピー装置２１２４である。更に、コンピュータシステム２１００とオーディオインターフェイスするために、スピーカ及び／又はマイクロホンのような音声記録及び再生装置をバス２１１１に任意に結合してもよい。バス２１１１に結合できる別の装置は、電話又はハンドヘルドパルム装置と通信するための有線／無線通信機能２１２５である。
【００９５】
[00116]システム２１００のコンポーネントのいずれか又は全部及びそれに関連したハードウェアを本発明に使用できることに注意されたい。しかしながら、コンピュータシステムの他のコンフィギュレーションがこれら装置の幾つか又は全部を含んでもよいことが明らかであろう。
【００９６】
[00117]当業者であれば、以上の説明を読んだ後に、本発明の多数の変更や修正が疑いなく明らかとなろうが、図示して説明した特定の実施形態は、本発明を何らそれに限定するものではないことを理解されたい。それ故、種々の実施形態の細部にわたる言及は、本発明の本質と考えられる特徴のみを記載した特許請求の範囲を限定するものではない。
【図面の簡単な説明】
【００９７】
【図１】プログラムコードをチェックするプロセスの一実施形態を示すフローチャートである。
【図２】予約が追加された４つのプログラムを示す図である。
【図３】コードコンシューマーのセキュリティポリシーによりプログラムに割り当てられた全てのリソースを最初に含む単一リソースプールを備えた典型的な動的リソースチェッカーを示す図である。
【図４】望ましいプールリソースモデルを示す図である。
【図５】予約による抽象リソース使用安全性を示す図である。
【図６】コード安全性を静的コンポーネント及び動的コンポーネントに仕切るところを示す図である。
【図７】標準的なバッカス記法で言語の一実施形態の完全な定義を示す図である。
【図８】注釈付け（コードプロダクションと共に）を遂行するコードプロデューサ、及び検証（実行と共に）を遂行するコンシューマーを示す図である。
【図９】コードコンシューマーが注釈付け及び検証を遂行するようにして、プロデューサとベリファイアとの間で考えられる基本的コンポーネントの別の分離を示す図である。
【図１０】ベリファイアの一実施形態を示すブロック図である。
【図１１】シーケンシング及び指定のためのオペレーションセマンティックスを示す図である。
【図１２】条件及びループのためのオペレーションセマンティックスを示す図である。
【図１３】予約のためのオペレーションセマンティックスを示す図である。
【図１４】安全条件ジェネレータのためのコードの一実施形態である。
【図１５】安全条件ジェネレータのフローチャートの一実施形態である。
【図１６】プローバーのためのコードの一実施形態である。
【図１７】プローバーを示すフローチャートである。
【図１８】ｗｈｉｌｅコマンドで書かれた小さなループを示す図である。
【図１９】この実施例に対する安全条件を示す図である。
【図２０】セルラー電話の一実施例のブロック図である。
【図２１】コンピュータシステムの一実施形態のブロック図である。
【符号の説明】
【００９８】
６００・・・コード、６０１・・・コンパイラー、６０３・・・マシン、１０００・・・ベリファイア、１００１・・・安全条件ジェネレータ、１００２・・・プローバー、２０１０・・・セルラー電話、２０１１・・・アンテナ、２０１２・・・ＲＦユニット、２０１３・・・モデム、２０１４・・・信号処理ユニット、２０１５・・・制御ユニット、２０１６・・・外部Ｉ／Ｆ、２０１７・・・スピーカ、２０１８・・・マイクロホン、２０１９・・・ディスプレイユニット、２０２０・・・操作ユニット、２０２１・・・メモリ
【図１】
2007516538.tif 000007
【図２】
2007516538.tif 000008
【図３】
2007516538.tif 000009
【図４】
2007516538.tif 000010
【図５】
2007516538.tif 000011
【図６】
2007516538.tif 000012
【図７】
2007516538.tif 000013
【図８】
2007516538.tif 000014
【図９】
2007516538.tif 000015
【図１０】
2007516538.tif 000016
【図１１】
2007516538.tif 000017
【図１２】
2007516538.tif 000018
【図１３】
2007516538.tif 000019
【図１４】
2007516538.tif 000020
【図１５】
2007516538.tif 000021
【図１６】
2007516538.tif 000022
【図１７】
2007516538.tif 000023
【図１８】
2007516538.tif 000024
【図１９】
2007516538.tif 000025
【図２０】
2007516538.tif 000026
【図２１】
2007516538.tif 000027
【手続補正書】
【提出日】平成18年6月26日(2006.6.26)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
プログラムコードを受け取るステップと、
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証するステップであって、前記プログラムコードにおける１つ以上の動的なチェックの各々が前記プログラムコードにおけるオペレーションをチェックするようなステップと、
を備える方法。
【請求項２】
前記動的なチェックの少なくとも１つは、オペレーションが非安全であるかどうか決定する、請求項１に記載の方法。
【請求項３】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、ランタイムの前に遂行される、請求項１に記載の方法。
【請求項４】
前記プログラムコードにおける１つ以上の動的なチェックに関してランタイムの前に情報を静的に検証する前記ステップは、安全性をチェックするためのものである、請求項１に記載の方法。
【請求項５】
前記１つ以上の動的なチェックの少なくとも１つは、リソース予約を指定するための１つ以上の注釈を含む、請求項１に記載の方法。
【請求項６】
前記リソース予約は、前記プログラムコードを安全に実行することに関連する、請求項５に記載の方法。
【請求項７】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが、ランタイム中に１つ以上のリソースのうち、前記プログラムコードが実行前に予約したものより多くを使用するかどうかチェックすることを含む、請求項１に記載の方法。
【請求項８】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが所定量より多くのリソースを使用するかどうかチェックすることを含む、請求項１に記載の方法。
【請求項９】
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、１つ以上のリソースを予約するために前記プログラムコードにおける第１セットのオペレーションの１つ以上を静的にチェックして、それら１つ以上のオペレーションにより予約される１つ以上のリソースが、前記プログラムコードにおいてリソースを消費する全てのランタイムオペレーションを考慮するに充分であるかどうか決定することを含む、請求項１に記載の方法。
【請求項１０】
１つ以上の動的なチェックを前記プログラムコードに追加するステップを更に備える、請求項１に記載の方法。
【請求項１１】
１つ以上の注釈を前記プログラムコードに追加するステップを更に備え、前記１つ以上の注釈の少なくとも１つは、前記プログラムコードの一部分により使用するためにリソースを予約するオペレーションを含む、請求項１に記載の方法。
【請求項１２】
少なくとも１つの静的なチェック及び少なくとも１つの動的なチェックの組合せを選択するステップと、
前記静的及び動的チェックを表すように前記プログラムコードに注釈を追加するステップと、
を更に備える請求項１１に記載の方法。
【請求項１３】
ランタイム中に前記動的チェックを呼び出すことにより前記プログラムコードの動的チェックを遂行するステップを更に備える、請求項１に記載の方法。
【請求項１４】
リソース使用が限界を越えたという決定に応答して前記プログラムコードによるリソース使用を制限するステップを更に備える、請求項１３に記載の方法。
【請求項１５】
前記プログラムコードによるリソース使用を制限する前記ステップは、前記プログラムコードの実行を停止する段階を含む、請求項１４に記載の方法。
【請求項１６】
リソース使用が限界を越えたという決定に応答して例外を生じさせるステップを更に備える、請求項１３に記載の方法。
【請求項１７】
リソース使用が限界を越えたという決定に応答して割り込みを発生するステップを更に備える、請求項１３に記載の方法。
【請求項１８】
前記１つ以上の動的なチェックの少なくとも１つは、リソースの使用をチェックするためのものである、請求項１に記載の方法。
【請求項１９】
前記リソースは物理的なリソースを含む、請求項１８に記載の方法。
【請求項２０】
前記物理的なリソースは、中央処理ユニット（ＣＰＵ）のインストラクションカウント、メモリスペース、ディスクスペース、ネットワーク帯域巾、装置ハードウェアオペレーション、及び装置ソフトウェアオペレーションより成るグループから選択されたものを含む、請求項１９に記載の方法。
【請求項２１】
前記リソースは仮想リソースを含む、請求項１８に記載の方法。
【請求項２２】
前記仮想リソースは、ファイルハンドル、プロセス、及びデータベース接続より成るグループから選択されたものを含む、請求項２１に記載の方法。
【請求項２３】
システムにより実行されたときに、システムが、
プログラムコードを受け取るステップと、
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証するステップであって、前記プログラムコードにおける１つ以上の動的なチェックの各々が前記プログラムコードにおけるオペレーションをチェックするためのものであるステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項２４】
前記動的なチェックの少なくとも１つは、オペレーションが非安全であるかどうか決定する、請求項２３に記載の製造物品。
【請求項２５】
前記１つ以上の動的なチェックの少なくとも１つは、リソース予約を指定するための１つ以上の注釈を含む、請求項２３に記載の製造物品。
【請求項２６】
１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、前記プログラムコードが、ランタイム中に１つ以上のリソースのうち、前記プログラムコードが実行前に予約したものより多くを使用するかどうかチェックすることを含む、請求項２３に記載の製造物品。
【請求項２７】
前記プログラムコードにおける１つ以上の動的なチェックに関する情報を静的に検証する前記ステップは、１つ以上のリソースを予約するために前記プログラムコードにおける第１セットのオペレーションの１つ以上を静的にチェックして、それら１つ以上のオペレーションにより予約される１つ以上のリソースが、前記プログラムコードにおいてリソースを消費する全てのランタイムオペレーションを考慮するに充分であるかどうか決定することを含む、請求項２３に記載の製造物品。
【請求項２８】
前記方法は、ランタイム中に前記動的チェックを呼び出すことにより前記プログラムコードの動的チェックを遂行するステップを更に備える、請求項２３に記載の製造物品。
【請求項２９】
前記方法は、リソース使用が限界を越えたという決定に応答して前記プログラムコードによるリソース使用を制限するステップを更に備える、請求項２８に記載の製造物品。
【請求項３０】
前記プログラムコードによるリソース使用を制限する前記ステップは、前記プログラムコードの実行を停止することを含む、請求項２９に記載の製造物品。
【請求項３１】
前記方法は、リソース使用が限界を越えたという決定に応答して例外を生じさせるステップを更に備える、請求項２８に記載の製造物品。
【請求項３２】
前記方法は、リソース使用が限界を越えたという決定に応答して割り込みを発生するステップを更に備える、請求項２８に記載の製造物品。
【請求項３３】
前記１つ以上の動的なチェックの少なくとも１つは、リソースの使用をチェックするためのものである、請求項２３に記載の製造物品。
【請求項３４】
リソースの式を静的に決定するステップと、
実行中にプログラムコードによるリソースの使用が限度内となるかどうかチェックできるようにする１つ以上の注釈を前記プログラムコードに追加するステップと、
を備えた方法。
【請求項３５】
前記限度は割当量によりセットされる、請求項３４に記載の方法。
【請求項３６】
システムにより実行されたときに、システムが、
リソースの式を静的に決定するステップと、
実行中にプログラムコードによるリソースの使用が限度内となるかどうかチェックできるようにする１つ以上の注釈を前記プログラムコードに追加するステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項３７】
注釈を有するプログラムコードを受け取るステップと、
取得したリソースが割当量より少ないかどうかチェックすることにより、前記プログラムコードを実行する間にリソース使用をチェックするステップと、
を備える方法。
【請求項３８】
前記プログラムコードにおける１つ以上の動的チェックに関する情報は、実行の前に静的に検証されている、請求項３７に記載の方法。
【請求項３９】
前記プログラムコードにおける１つ以上の動的チェックに関する情報は、１つ以上の動的チェックの各々に関連したプログラムコードにおけるオペレーションの実行前に静的に検証されている、請求項３７に記載の方法。
【請求項４０】
システムにより実行されたときに、システムが、
注釈を有するプログラムコードをダウンロードするステップと、
取得したリソースが割当量より少ないかどうかチェックすることにより、前記プログラムコードを実行する間にリソース使用をチェックするステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項４１】
ランタイム中に１つ以上のリソースの使用を動的に要求するプログラムコードを受け取るステップと、
前記プログラムコードを静的にチェックして、前記プログラムコードがランタイム中に許可されたリソースしか使用しないことを決定するステップと、
を備える方法。
【請求項４２】
システムにより実行されたときに、システムが、
ランタイム中に１つ以上のリソースの使用を動的に要求するプログラムコードを受け取るステップと、
前記プログラムコードを静的にチェックして、前記プログラムコードがランタイム中に許可されたリソースしか使用しないことを決定するステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【国際調査報告】
2007516538.tif 000028
2007516538.tif 000029
2007516538.tif 000030