Secure Coding mailing list archives
Re: Strategies for teaching secure coding practices
From: Crispin Cowan <crispin () immunix com>
Date: Mon, 15 Dec 2003 03:22:21 +0000
Brian Chess wrote: David Crocker wrote: An alternative way is to *prove* that all inputs are within bounds ... This approach is more or less impossible to apply if you are coding in C or C++. It may be feasible if you are using Java (using tools such as ESC/Java) ... Funny you should mention that. My dissertation focused on showing that you can apply Extended Static Checking to the problem of finding some common types of security vulnerabilities in real C programs. (Common types of security vulnerabilities being things like buffer overflow, race conditions, and format string vulnerabilities.) In type-unsafe languages like C, where you can do arbitrary arithmetic on a void * pointer, proving type safety is semi-decidable. You can *sometimes* prove that a C program is type safe, a trivial example being to look for pointer arithmetic, and if the program doesn't use pointer arithmetic then it is much easier to prove type safety. Unfortunately, many C programs contain enough type-unsafe crap that it is impractical to prove type safety, in many cases because the program is type-unsafe :) The difference between what David speaks of and what Brian speaks of is that David hopes to prove that a program is safe, while Brian can detect that a program is unsafe. This may sound like two sides of the same coin, but in practice there is a large gap between the two: undecidable C programs that don't have detectable vulnerabilities, but also cannot be proven to be safe. The main advantage of type safe languages like Java and ML is to close that gap. Where you *cannot* close the gap (must run a large C application that cannot be proved safe) we provide run-time intrusion prevention tools in Immunix OS: StackGuard, FormatGuard, SubDomain, etc. Marketing crap deleted for your convenience, but you can read about it here http://www.immunix.com/shop/ and here http://www.immunix.org/ Crispin -- Crispin Cowan, Ph.D. http://immunix.com/~crispin/ CTO, Immunix http://immunix.com Immunix 7.3 http://www.immunix.com/shop/
Current thread:
- Re: Strategies for teaching secure coding practices, (continued)
- Re: Strategies for teaching secure coding practices Keith Watson (Dec 12)
- Re: Strategies for teaching secure coding practices Steve Litt (Dec 12)
- Re: Strategies for teaching secure coding practices Andrew Gray (Dec 12)
- Re: Strategies for teaching secure coding practices David Evans (Dec 12)
- Re: Strategies for teaching secure coding practices Dana Epp (Dec 12)
- Re: Strategies for teaching secure coding practices Crispin Cowan (Dec 12)
- RE: Strategies for teaching secure coding practices David Crocker (Dec 13)
- Re: Strategies for teaching secure coding practices Crispin Cowan (Dec 13)
- RE: Strategies for teaching secure coding practices David Crocker (Dec 14)
- Re: Strategies for teaching secure coding practices Brian Chess (Dec 14)
- Re: Strategies for teaching secure coding practices Crispin Cowan (Dec 14)
- RE: Strategies for teaching secure coding practices David Crocker (Dec 13)
- Re: Strategies for teaching secure coding practices Jeff Williams @ Aspect (Dec 13)