Splint - Secure Programming Lint
|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 ProjectsGasta - Guillaume Thouvenin's GCC AST Analysis Project is working on automatically producing Splint annotations.
Programming the Swarm
Information Survivability for Critical Infrastructure Protection
Related Research ProjectsAlloy AnalyzerMIT'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 LanguageSun'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 ToolkitDaniel 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 CheckingProject at DEC Systems Research Center using theorem proving technology to enable extensive static checking in Java and Modula-3.CycloneCyclone is a safe dialect of C developed by AT&T Labs Research and Greg Morrisett's group at Cornell University.Open Source Quality ProjectBerkeley'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 GroupResearch group at Stanford University led by David Luckham.SLAM ProjectThe 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.VaultVault 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 ToolsSome commercial tools have been developed that focus on static checking, some can be used to check for conformance to various standards.
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 ToolsSplint 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
LarchMIT 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 ProgrammingBuilding Secure Software - web site for John Viega and Gary McGraw's book.
Common Vulnerabilities and Exposures
Secure Programming for Linux and Unix HOWTO by David A. Wheeler (a freely-available and detailed book on how to write secure programs)
Reverse LinksLinks to some publications and web pages that reference Splint.
BooksSecure 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 reviewC 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 KellyIncludes 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
FAQsC 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 ArticlesThe 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.
CoursesThese 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 SitesLysator Programming in C (under Other Sources)
Association of C and C++ Users
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
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