Splint - Secure Programming Lint
[email protected]
Download - Documentation - Manual - Links Reporting Bugs - Mailing Lists      Sponsors - Credits

Splint Related Links

This page collects some of the more interesting links related to Splint and static checking. This page is not updated, and preserved only for historical interest.

Connected Projects

Gasta - Guillaume Thouvenin's GCC AST Analysis Project is working on automatically producing Splint annotations.
Programming the Swarm
Information Survivability for Critical Infrastructure Protection
CS588: Cryptology

Related Research Projects

Alloy Analyzer
MIT's Software Design Group focuses on new kinds of tools: design checkers and error analyzers, among others. The Alloy Analyzer analyzes models written in Alloy.
Assertion Definition Language
Sun's ADL is a formal specification language for C programs. The ADLT tool can be used to automate testing using an ADL specification. They like to make unfounded claims about it being the first ever practical specification language.
AST Toolkit
Daniel Weise's group at Microsoft Research is working on toolkits for analyzing program parse trees. Their AST Toolkit supports some LCLint-derivative checks.
Berkeley Analysis Engine (BANE)
BANE is a toolkit for constructing program analyses such as dataflow and type inference systems developed by Alex Aiken.
Extended Static Checking
Project at DEC Systems Research Center using theorem proving technology to enable extensive static checking in Java and Modula-3.
Cyclone
Cyclone is a safe dialect of C developed by AT&T Labs Research and Greg Morrisett's group at Cornell University.
Open Source Quality Project
Berkeley's project on techniques and tools for assuring software qualify. Focuses on formal verification and theorem proving, model checking, and large-scale software analysis.
Program Analysis and Verification Group
Research group at Stanford University led by David Luckham.
SLAM Project
The Software Productivity Tools Research group at Microsoft Research investigates relationships between Software (Specifications), Languages, Analysis, and Model checking. Their goal is to be able to check that software satisfies critical behavioral properties of the interfaces it uses, and to aid software engineers in designing interfaces and software to ensure reliable and correct functioning.
Vault
Vault is a safe version of the C programming language developed by Microsoft Research's Software Productivity Tools research group. Because of the language restrictions and sophisticated analyses, Vault can enforce many of the properties Splint checks soundly and completely.

Commercial Static Analysis Tools

Some commercial tools have been developed that focus on static checking, some can be used to check for conformance to various standards.
  • Abraxas's CodeCheck
  • CenterLine's C++Expert does both compile-time and run-time checking. It incorporates checks based on Scott Meyer's "Effective C++" books.
  • Gimpel's PC-Lint
  • Cigital's ITS4 scans code for possible security flaws
  • Knowledge Software's Open Systems Protability Checker
  • McCabe & Associates offer a suite of tools and methodology that will assist software developers with software quality assurance, software testing, software reengineering and Year 2000 efforts.
  • Parasoft's Code Wizard is a source code analysis tool for C++, also based on Scott Meyer's books.
  • Intrinsa's Software Component Simulation uses simulation to detect software defects. (Note: Intrinsa was bought by Microsoft and seems to have no web presence remaining. The PREfix tool is widely used within Microsoft.)
  • PolySpace sells a C Verifier that uses abstract interpretation techniques to detect potential run-time errors (including array bounds errors).
  • Programming Research offers QA/C, a static checking tool including code metrics.
  • RATS - rough auditing tool for security
  • Scientific Toolworks produces tools that analyze Ada, C, C++ and FORTRAN source code to reverse engineer and automatically document programms.
  • Run-Time Checking Tools

    Splint hopes to extend the scope of what is checked statically, but there are many types of errors that are still only detectable at run-time. Several commercial and research tools focus on detecting dynamic memory errors are run-time.
  • Valgrind is an open-source memory debugger for x86 GNU-Linux
  • CenterLine's C++Expert also does run-time memory checking. Scott Meyer's "Effective C++" books.
  • Great Circle is a glorified garbage collector.
  • Immunix StackGuard
  • Numega's Bounds Checker
  • Parasoft's Insure++
  • Rational Software's Purify
  • The National Physical Laboratory of the United Kingdom offers an ISO C validation service. It uses both static and dynamic checking.
  • Some other tools are listed at Ben Zorn's Debugging Tools for Dynamic Storage Allocation page
  • Formal Methods

    Larch

    MIT Larch Page
    Jim Horning's Larch Page

    Larch C++

    A Larch Interface Language for C++ developed by Gary Leavens and others at Iowa State. Currently there is nothing equivalent to Splint for Larch/C++.
    Software Verification mailing list
    Formal Methods Page

    Secure Programming

    Building Secure Software - web site for John Viega and Gary McGraw's book.
    Cigital
    Common Vulnerabilities and Exposures
    Linux Security
    Secure Programming for Linux and Unix HOWTO by David A. Wheeler (a freely-available and detailed book on how to write secure programs)
    SecurityFocus

    Reverse Links

    Links to some publications and web pages that reference Splint.

    Books

    Secure Coding: Principles and Practices, by Mark G. Graff and Kenneth R. van Wyk, O'Reilly, 2003.

    David Hanson's book C Interfaces and Implementations advocates a design methodology based on interfaces and implementations very similar to that supported by Splint.

    However, if more C programmers read, understood, and imitated this book, the world would be a better and safer place. --- From Richard O'Keefe's review
    C Unleashed, by Richard Heathfield, Lawrence Kirby, Mike Lee, Mathew Watson, Ben Pfaff, Dann Corbit, Peter Seebach, Brett Fishburne, Scott Fluhrer, Ian Woods, Sam Hobbs, Ian Kelly
    Includes a short section describing running Splint with +strict and +checks on a 3-line program.
    Cryptography in C and C++, by Michael Welschenbach, David Kramer

    FAQs

    C Frequently Asked Questions (also published as a book by Addison-Wesley in 1995) Note the Splint information is out-of-date, but the C FAQ is no longer being updated.

    LCLint is also mentioned in its evil twin, the comp.lang.c Infrequently Asked Questions file (unfortunately, the entry for LCLint hasn't been true since before Version 2.0, but I'm counting on them to come up with a more suitable entry in the next edition.)

    Linux Frequently Asked Questions

    Linux GCC FAQ

    Catalog of Free Compilers and Interpreters

    Shmoo Group's How to Write Secure Code

    David Wheeler's Secure Programming for Linux and Unix HOWTO

    Magazine Articles

    The German Computer Magazine c't describes Splint in the article Fehlersuche in Java in its 4/2004 issue (full article not available on line, just links).

    Linux Journal, The Code Analyser LCLint. By David Santo Orcero, May 2000.
        “Debugging code is never fun, but this tool makes it a bit easier.”

    Linux Gazette, Static checking of C programs with LCLint. By Pramode C E and Gopakumar C E. Issue 51, March 2000.
        “LCLint is justifiably angry at such amateurish use of C, but he is gentle in his admonishments.”

    The German computer magazine, Ix, includes LCLint in an article, Lint als C-Syntax-Prufer in the July 96 issue.

    MATLAB Digest, Checking Code and Models in Production Environments, July 2003. Focuses on checking standard compliance.

    Courses

    These courses either use Splint (or used LCLint) in a programming lab, or include Splint technical papers. If you know of any other courses that should be listed here, please let me know.
    Second Year programming lab at the Imperial College of Science, Technology and Medicine, University of London.
    Steve Linton's lectures on Larch at University of St. Andrews, Scotland.
    Daniel Jackson's Tractable Representations for Software Development course at Carnegie Mellon.
    University of Cincinatti
    University of Washington CSE 503 l2D5333 Programverifiering, kursuppl�ggning at the Royal Institute of Technology, Stockholm.
    Programmeringsmetodik at Uppsala University in Sweden.
    Databehandlingslaboratorium at the University of Oslo.
    Richard O'Keefe's Systems Programming 1 course at RMIT University in Melbourne, Australia.

    Web Sites

    Lysator Programming in C (under Other Sources)
    Association of C and C++ Users
    Linux Links
    Free On-Line Dictionary of Computing
    US Department of Agriculture, Information Technology Center
    R. Nassif's Programming Page
    Modern Web Programming
    Sterling Software Archives in programming tools
    Ecole Nationale Supirieure de Techniques Avancies, in Unix Programming
    Internet Goodies in unix programming
    Herbert Dietze's collection of useful programming information

    More Links

    Search Google for links to lclint.cs.virginia.edu
    Search Google for links to www.splint.org
    Search Google for mentions of LCLint
    Search Google for mentions of Splint

    Splint - Secure Programming Lint [email protected]
    Download - Documentation - Manual - Links
    Source - Linux - Publications - Talks
    Reporting Bugs    Sponsors - Credits