Skip to main content

Currently Skimming:

Programming Methodology
Pages 102-123

The Chapter Skim interface presents what we've algorithmically identified as the most significant single chunk of text within every page in the chapter.
Select key terms on the right to highlight them within pages of the chapter.


From page 102...
... Critical software needs to work very well almost all of the time, and certain kinds of failures must be avoided. Critical software is used in trusted and safety-critical applications, for example, medical instruments, where failure of the software can have catastrophic results.
From page 103...
... Producing it presents the same problems as does producing critical software, plus some others. One of the key problems is analyzing the kinds of attacks that the software must be designed to resist.
From page 104...
... Because security cannot be attained without quality and the environment in which a system is to run is usually hard to control, typically one must either remove performance constraints (perhaps by allocating extra resources) or reduce the intended functionality.
From page 105...
... Secure software should be accompanied by instructions and tools that make it possible to do continuing quality assurance in the field. Software delivered without assurance evidence may provide only illusory security.
From page 106...
... This can lead developers to compromise the structure or integrity of code or to employ intricate fast algorithms, responses that almost always make the software harder to produce and less reliable, and often make it more dependent on the precise characteristics of the input. Better hardware and less ambitious specifications deserve strong consideration before one ventures into such an exercise in software
From page 107...
... . · Higher-level languages provide checkable redundancy, such as type checking that can turn programs with unintended semantics into illegal programs that are rejected by the compiler.
From page 108...
... Thus specifications provide logical firewalls between providers and clients of abstractions. During system auditing, specifications provide information that can be used to generate test data, build stubs, and analyze information flow.
From page 109...
... Design verification has enjoyed considerable success both inside and outside the security area. The key to this success has been that the conjectures to be checked and the specifications from which they are supposed to follow can both be written at the same relatively high level of abstraction.
From page 110...
... Informal but rigorous reasoning about the relationships between implementations and specifications has proved to be an effective approach to finding errors (Solomon, 1982~. People building concurrent programs frequently state key invariants and make informal arguments about their validity (Lamport, 1989; Wing, 1990~.
From page 111...
... The process of formally verifying that a program is correct with respect to its specification involves both generating and proving verification conditions. A verification-condition generator accepts as input a piece of code and formal specifications for that code, and then outputs a set of verification conditions, also called conjectures or proof obligations.
From page 112...
... Organizations building secure systems have made serious attempts to apply formal specification, formal design verification, and formal program verification. This committee interviewed members of several such organizations4 and observed a consistent pattern: · Writing formal specifications and doing design verification significantly increased people's confidence in the quality of their designs.
From page 113...
... · More attention needs to be devoted to formalizing a variety of generally applicable security properties that can be verified at the design level. · Little is understood about the formal specification and verification of performance constraints.
From page 114...
... For similar reasons it is usually prudent to stick to established tools when building software that must be secure. Not only should programmers use programming languages they already understand, but they should also look for compilers that have been used extensively in similar projects.
From page 115...
... could be interpreted as virtually mandating such a relationship. If implemented, this act, which would stop the flow of "inside" information to potential vendors, might have the effect of stopping the flow of all information to potential vendors, thus significantly increasing the number of government software procurements that would overrun costs or fail to meet the customer's expectations.5 2.
From page 116...
... Finally, buying software from the lowest bidder encourages vendors to take a short-term approach to software development. In a well-run software organization, every significant software project should have as a secondary goal producing components that will be useful in other projects.
From page 117...
... There is a more serious shortage of those qualified to build critical software, and a dramatic shortage of people qualified to build secure software. A discussion of the general shortage of qualified technical people in this country is beyond the scope of this report.
From page 118...
... The two efforts are typically conducted by different teams that have different outlooks and use different notations. In general, the assurance team has an analytical outlook that is reflected in the notations it uses to describe a system; the development team focuses on the timely production of software, and accordingly emphasizes synthesis and creativity.
From page 119...
... This means more than merely running regression tests. If, for example, assurance involves covert channel analyses, then those too must be redone.
From page 120...
... Attempts to provide protection from high-grade threats by strictly limiting the number of people with access to various parts of the software may be self-defeating. The social process of the interaction of professionals on a project, conducted formally or casually, is a powerful tool for achieving correctness in fields like mathematics or software that deal with intangibles.
From page 121...
... · Finding: The use of higher-level programming languages reduces the probability of residual errors, which in turn reduces the probability of residual vulnerabilities. Recommendation: When tunneling attacks are not a major concern, use higher-level languages in building secure software.
From page 122...
... Recommendation: Establish educational programs that emphasize the construction of trusted and secure software in the context of software engineering. · Finding: Adopting new software production practices involves a substantial risk that cannot usually be undertaken without convincing evidence that significant benefits are likely to result.
From page 123...
... PROG^~G ~E~ODOLOGY 123 Technology Corporation Jormedy Honeydew Acme Computing Technology Chart and George Dipole Ford Aerospace Corporabon. ~ Im~emen~tion of the Pro~em~t Inanity Act of 1989 as Resided through November 30, 1990, and may be Other suspended Eta May 31, 1991, to consider proposed changes by the Adm~is~abon (see Concessions Record of June 21, 1990, ad August 2, 19907


This material may be derived from roughly machine-read images, and so is provided only to facilitate research.
More information on Chapter Skim is available.