appE - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: Appendix D Specifications（仕様）

Next: End Notes（文末脚注）

Section：1　2　3　4　5　6　7　8　9　10　11　12　13　14　A　B　C　D　E

Appendix E Annotated Bibliography（文献解題）

Splint

これらの論文はすべて、http://www.splint.org/publications/(英)から利用可能です。

[Barker01] Chris Barker（著）。Static Error Checking of C Applications Ported from UNIX to WIN32 Systems Using LCLint（LCLintを使用してのUnixからWin32システムへ移植されたC言語アプリケーションの静的エラーチェック）。ヴァージニア大学コンピューター工学部、卒業研究。2001年5月。

移植するアプリケーションに対するアノテーションと有益なチェックについて述べています。

[Evans94] David Evans（著）。 Using specifications to check source code（ソースコードをチェックするために仕様を使用すること）。 MIT/LCS/TR 628、コンピュータ科学のための研究室、マサチューセッツ工科大学、1994年6月。

MITのSMの論文（訳注：元々略語で書かれていたため、確定できないが、恐らくは、MIT：マサチューセッツ工科大学、SM：ソフトウェアメンテナンス。）。どのような仕様が軽いチェックをするために利用できるかに焦点を当て、Splintの背後に研究を説明しています。LCLintを使用したケーススタディが含まれています。

[EGHT94] David Evans、 John Guttag、 Jim Horning 、Yang Meng Tan（著）。LCLint: A tool for using specifications to check code（LCLint：コードをチェックするために仕様を使用するためのツール）。SIGSOFT Symposium on the Foundations of Software Engineering、1994年12月。

LCLintへの、やや時代遅れの紹介。 LCLintをサンプルプログラム内のエラーを発見するために使用する方法を示しています。

[Evans96] David Evans（著）。Static Detection of Dynamic Memory Errors（動的メモリエラーの静的検出）。プログラミング言語の設計と実装に関するSIGPLAN会議（PLDI'96）、ペンシルバニア州フィラデルフィア。1996年5月。

多くの種類のエラーを検知するために追加されたアノテーションを活用するための手法について説明しています。このマニュアルのSection 5で説明したメモリ管理チェックに重点を置いています。

[Evans00] David Evans（著）。Annotation-Assisted Lightweight Static Checking（アノテーションで支援された軽い静的チェック）。自動化されたプログラムの解析、テストと検証に関する第1回国際ワークショップ、 2000年2月。

Splintの後ろで研究課題を記述した短い方針提案です。

[Evans02] David Evans、 David Larochelle（著）。Improving Security Using Extensible Lightweight Static Analysis（拡張可能な軽い静的解析を使用してのセキュリティの向上）。IEEE Software、2002年1月/2月。

ほとんどのセキュリティ攻撃は、実装の欠陥がよく知られているクラスのインスタンスを利用します。この記事では、Splintを、（バッファオーバーフローや書式文字列の脆弱性を含む）一般的なセキュリティの脆弱性を検出するために使用する方法について説明します。

[Larochelle01] David Larochelle 、 David Evans（著）。Statically Detecting Likely Buffer Overflow Vulnerabilities(バッファーオーバーフロー脆弱性の可能性を静的に検知する)。2001年USENIXセキュリティシンポジウム、ワシントン、D. C.、2001年8月13日-17日。

バッファーオーバーフロー攻撃は、今日の最も重要なセキュリティ上の脅威となることがあります。この論文では2つのセキュリティに敏感なプログラム内でバッファーオーバーフロー脆弱性を検知するために、私たちの方法を使用したプログラムソースコードの解析や現在の経験を通して脆弱性の可能性を検知するためにSplintを使用する方法について述べています。

C

[ISO99] 国際標準ISO/ IEC9899（著）。Programming languages – C(プログラミング言語-C)。第2版。1999年12月。

Cプログラミング言語の国際標準規格です。 ANSI2000年5月に承認されました。

[KR88] Brian W. Kernighan 、 Dennis M. Ritchie（著）。The C Programming Language(プログラミング言語C)。第2版。Prentice Hall, New Jersey。1988年

ANSI Cの標準的な参考書です。この1冊を聞いたことが無い場合、（後ろで始めてない限りは）おそらくここまで取得していません。

[vdL94] Peter van der Linden（著）。Expert C Programming: Deep C Secrets(エキスパートCプログラミング―知られざるCの深層)。SunSoft Press, Prentice Hall, New Jersey。1994年

C言語の暗い隅の便利な情報だけではなく、業界の逸話やユーモアで満たされています。Splintの予約名チェックはこの本の中で予約されている名前のリストに緩く基づいています。

Methodology

[GH93] John Guttag 、James Horning with Stephen J. Garland, Kevin D. Jones、 Andrés Modet　、 Jeannette M. Wing（著）。Larch: Languages and Tools for Formal Specification(ラーチ：形式仕様に対する言語とツール)。Springer-Verlag、Texts and Monographs in Computer Science。1993年

仕様言語と関連ツールのラーチファミリーの概要です。Splintの元になっているLCL(ラーチCインタフェース言語）の章があります。

[LG86] Barbara Liskov 、John Guttag（著）。Abstraction and Specification in Program Development(プログラム開発の抽象化と仕様)。MIT Press, Cambridge、 MA。1986年

抽象型と指定されたインタフェースを使用したプログラミング方法について説明します。Splintの基礎となる方法論の多くは、この本から来ています。 CLUプログラミング言語を使用しています。

[Liskov01] Barbara Liskov 、John Guttag（著）。Program Development in Java(Javaでのプログラム開発)。Addison Wesley。2001年

Javaプログラミング言語のための[LG86]のアップデート版です。

[Tan95] Yang Meng Tan（著）。Formal Specification Techniques for Engineering Modular C(エンジニアリングモジュラーC用の形式仕様のテクニック)。Kluwer International Series in Software Engineering, Volume 1, Kluwer Academic Publishers, Boston、1995年。

MITのPh D論文の修正・更新版であり、以前はMIT/LCS/TR-619, 1994として公開されていました。LCLの意味論の紹介とLCLを使用してのケーススタディが含まれています。

Secure Programming

[Hat95] Les Hatton（著）。Safer C: Developing Software for High-integrity and Safety-critical Systems(より安全なC言語：高整合性とセーフティクリティカルシステムのためのソフトウェア開発)。McGraw-Hill International Series in Software Engineering。1995年

C言語に焦点を当て、セーフティクリティカルなソフトウェアの開発のあらゆる側面に関する幅広い仕事です。セーフクリティカルシステムにおけるC言語の使用に対して良い理由付けと、ツールでサポートされているプログラミング標準の必要性を提供します。Splintの使用者は、動的にしか検出できないこととしてリスト化されているエラーの多くが、どのようにしてSplintによって静的に検出されるのかを見ることは興味があることでしょう。

[VM02] John Viega 、Gary McGraw（著）。Building Secure Software: How to Avoid Security Problems the Right Way(安全なソフトウェアの構築：セキュリティ問題を正しい方法で回避する方法)。Addison-Wesley、2002年

安全なプログラムを構築するための手法と原則を包括的に調査しています。

[Evans02] と [Larochelle01]も参照してください。

このドキュメントはSplint(英)のサイトを元に作成しました

Up: マニュアル

Prev: Appendix D Specifications（仕様）

Next: End Notes（文末脚注）