Annex Outline
Yüklə 77 Kb.
|
 ISO/IEC JTC 1/SC 22/WG 23 N 03XX December 2011
ISO/IEC JTC 1/SC 22/WG 23 N 0384 Draft language-specific annex for SPARK
Annex SPARK(informative) SPARK. Vulnerability descriptions for the language SPARKSPARK.0 Status and history
SPARK.1 Identification of standards and associated documentationSee Ada.1, plus the references below. In the body of this annex, the following documents are referenced using the short abbreviation that introduces each document, optionally followed by a specific section number. For example “[SLRM 5.2]” refers to section 5.2 of the SPARK Language Definition. [SLRM] SPARK Language Definition: “SPARK95: The SPADE Ada Kernel (Including RavenSPARK)” Latest version always available from www.altran-praxis.com. [SB] “High Integrity Software: The SPARK Approach to Safety and Security.” John Barnes. Addison-Wesley, 2003. ISBN 0-321-13616-0. [IFA] “Information-Flow and Data-Flow Analysis of while-Programs.” Bernard Carré and Jean-Francois Bergeretti, ACM Transactions on Programming Languages and Systems (TOPLAS) Vol. 7 No. 1, January 1985. pp 37-61. [LSP] “A behavioral notion of subtyping.” Barbara Liskov and Jeannette Wing. ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 16, Issue 6 (November 1994), pp. 1811 - 1841.
SPARK.2 General terminology and conceptsThe SPARK language is a contractualized subset of Ada, specifically designed for high-assurance systems. SPARK is designed to be amenable to various forms of static analysis that prevent or mitigate the vulnerabilities described in this TR. Many terms and concepts applicable to Ada also apply to SPARK. See Ada.2. This section introduces concepts and terminology which are specific to SPARK and/or relate to the use of static analysis tools.
This concept relates to the absence of false-negative results from a static analysis tool. A false negative is when a tool is posed the question “Does this program exhibit vulnerability X?” but incorrectly responds “no.” Such a tool is said to be unsound for vulnerability X. A sound tool effectively finds all the vulnerabilities of a particular class, whereas an unsound tool only finds some of them. The provision of soundness in static analysis is problematic, mainly owing to the presence of unspecified and undefined features in programming languages. Claims of soundness made by tool vendors should be carefully evaluated to verify that they are reasonable for a particular language, compilers and target machines. Soundness claims are always underpinned by assumptions (for example, regarding the reliability of memory, the correctness of compiled code and so on) that should also be validated by users for their appropriateness. Static analysis techniques can also be sound in theory – where the mathematical model for the language semantics and analysis techniques have been formally stated, proved, and reviewed – but unsound in practice owing to defects in the implementation of analysis tools. Again, users should seek evidence to support any soundness claim made by language designers and tool vendors. A language which is unsound in theory can never be sound in practice. The single overriding design goal of SPARK is the provision of a static analysis framework which is sound in theory, and as sound in practice as is reasonably possible. In the subsections below, we say that SPARK prevents a vulnerability if supported by a form of static analysis which is sound in theory. Otherwise, we say that SPARK mitigates a particular vulnerability. SPARK Processor We define a “SPARK Processor” to be a tool that implements the various forms of static analysis required by the SPARK language definition. Without a SPARK Processor, a program cannot reasonably be claimed to be SPARK at all, much in the same way as a compiler checks the static semantic rules of a standard programming language. In SPARK, certain forms of analysis are said to be mandatory – they are required to be implemented and programs must pass these checks to be valid SPARK. Examples of mandatory analyses are the enforcement of the SPARK language subset, static semantic analysis (e.g. enhanced type checking) and information flow analysis [IFA]. Some analyses are said to be optional – a user may choose to enable these additional analyses at their discretion. The most notable example of an optional analysis in SPARK is the generation of verification conditions and their proof using a theorem proving tool. Optional analyses may provide greater depth of analysis, protection from additional vulnerabilities, and so on, at the cost of greater analysis time and effort. Failure modes for static analysis Unlike a language compiler, a user can always choose not to, or might just forget to run a static analysis tool. Therefore, there are two modes of failure that apply to all vulnerabilities:
SPARK.3 Type System [IHN]SPARK mitigates this vulnerability. SPARK’s type system is a simplification of that of Ada. Both Explicit and Implicit conversions are permitted in SPARK, as is instantiation and use of Unchecked_Conversion [SB 1.3]. A design goal of SPARK is the provision of static type safety, meaning that programs can be shown to be free from all run-time type failures using entirely static analysis. If this optional analysis is achieved, a SPARK program should never raise an exception at run-time.
SPARK.4 Bit Representation [STR]SPARK mitigates this vulnerability. SPARK is designed to offer a semantics which is independent of the underlying representation chosen by a compiler for a particular target machine. Representation clauses are permitted, but these do not affect the semantics as seen by a static analysis tool [SB 1.3]. SPARK.5 Floating-point Arithmetic [PLF]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.5 [PLF]. SPARK.6 Enumerator Issues [CCB]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.6 [CCB]. SPARK.7 Numeric Conversion Errors [FLC]SPARK prevents this vulnerability. SPARK is designed to be amenable to static verification of the absence of predefined exceptions, and in particular all cases covered by this vulnerability [SB 11]. All numeric conversions (both explicit and implicit) give rise to a verification condition that must be discharged, typically using an automated theorem-prover. SPARK.8 String Termination [CJM]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.8 [CJM]. SPARK.9 Buffer Boundary Violation (Buffer Overflow) [HCB]SPARK prevents this vulnerability. SPARK is designed to permit static analysis for all such boundary violations, through techniques such as theorem proving or abstract interpretation [SB 11]. SPARK programs that have been subject to this level of analysis can be compiled with run-time checks suppressed, supported by a body of evidence that such checks could never fail, and thus removing the possibility of erroneous execution.
SPARK.10 Unchecked Array Indexing [XYZ]SPARK prevents this vulnerability. See SPARK.9. SPARK.11 Unchecked Array Copying [XYW]SPARK prevents this vulnerability. Array assignments in SPARK are only permitted between objects that have statically matching bounds, so there is no possibility of an exception being raised [SB 5.5, SLRM 4.1.2]. Ada’s “slicing” and “sliding” of arrays is not permitted in SPARK, so this vulnerability cannot occur. SPARK.12 Pointer Casting and Pointer Type Changes [HFC]SPARK prevents this vulnerability. This vulnerability cannot occur in SPARK, since the SPARK subset forbids the declaration or use of access (pointer) types [SB 1.3, SLRM 3.10]. SPARK.13 Pointer Arithmetic [RVG]SPARK prevents this vulnerability. See SPARK.12. SPARK.14 Null Pointer Dereference [XYH]SPARK prevents this vulnerability. See SPARK.12. SPARK.15 Dangling Reference to Heap [XYK]SPARK prevents this vulnerability. See SPARK.12. SPARK.16 Arithmetic Wrap-around Error [FIF]See Ada.16 [FIF]. In addition, SPARK mitigates this vulnerability through static analysis to show that a signed integer expression can never overflow at run-time [SB 11]. SPARK.17 Using Shift Operations for Multiplication and Division [PIK]SPARK is identical to Ada with respect to this vulnerability and is mitigation. See Ada.17 [PIK]. SPARK.18 Sign Extension Error [XZI]SPARK is identical to Ada with respect to this vulnerability and is mitigation. See Ada.18 [XZI]. SPARK.19 Choice of Clear Names [NAI]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.19 [NAI]. SPARK.20 Dead store [WXQ]SPARK prevents this vulnerability through mandatory static information flow analysis [IFA], which detects dead stores. Additionally, SPARK requires variables that are used for output to the environment, or for communication between tasks to be specifically identified. IFA for such variables is modified since it is know that consecutives writes to such variables might not constitute a dead store. SPARK.21 Unused Variable [YZS]SPARK mitigates this vulnerability. As in Ada.21 [YZS]. Also, SPARK is designed to permit sound static analysis of the following cases [IFA]:
SPARK.22 Identifier Name Reuse [YOW]SPARK prevents this vulnerability. This vulnerability is prevented through language rules enforced by static analysis. SPARK does not permit names in local scopes to redeclare and hide names that are already visible in outer scopes [SLRM 6.1]. SPARK.23 Namespace Issues [BJL]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.23 [BJL]. SPARK.24 Initialization of Variables [LAV]SPARK prevents this vulnerability through mandatory static information flow analysis [IFA]. SPARK.25 Operator Precedence/Order of Evaluation [JCW]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.25 [JCW]. SPARK.26 Side-effects and Order of Evaluation [SAM]SPARK prevents this vulnerability. SPARK does not permit functions to have side-effects, so all expressions are side-effect free. Static analysis of run-time errors also ensures that expressions evaluate without raising exceptions. Therefore, expressions are neutral to evaluation order and this vulnerability does not occur in SPARK [SLRM 6.1]. SPARK.27 Likely Incorrect Expression [KOA]SPARK is identical to Ada with respect to this vulnerability and its mitigation (see Ada.3.KOA) although many cases of “likely incorrect” expressions in Ada are forbidden in SPARK. SPARK.28 Dead and Deactivated Code [XYQ]SPARK mitigates this vulnerability. In addition to the advice of Ada.28 [XYQ], SPARK is amenable to optional static analysis of dead paths. A dead path cannot be executed in that the combination of conditions for its execution are logically equivalent to false. Such cases can be statically detected by theorem proving in SPARK. SPARK.29 Switch Statements and Static Analysis [CLL]As in Ada.29 [CLL], this vulnerability is prevented by SPARK. The vulnerability relating to an uninitialized variable and the “when others” clause in a case statement is also prevented – see SPARK.24 [LAV]. SPARK.30 Demarcation of Control Flow [EOJ]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.30 [EOJ]. SPARK.31 Loop Control Variables [TEX]SPARK prevents this vulnerability in the same way as Ada. See Ada.31 [TEX]. SPARK.32 Off-by-one Error [XZH]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.32 [XZH]. Additionally, any off-by-one error that gives rise to the potential for a buffer-overflow, range violation, or any other construct that could give rise to a predefined exception, will be detected by static analysis in SPARK [SB 11]. SPARK.33 Structured Programming [EWD]SPARK mitigates this vulnerability. Several of the vulnerabilities in this category that affect Ada are entirely eliminated by SPARK. In particular: the use of the goto statement is prohibited in SPARK [SLRM 5.8], loop exit statements only apply to the most closely enclosing loop (so “multi-level loop exits” are not permitted) [SLRM 5.7], and all subprograms have a single entry and a single exit point [SLRM 6]. Finally, functions in SPARK must have exactly one return statement which must the final statement in the function body [SLRM 6]. SPARK.34 Passing Parameters and Return Values [CSJ]SPARK mitigates this vulnerability. SPARK goes further than Ada with regard to this vulnerability. Specifically;
Both of these properties can be checked by static analysis. SPARK.35 Dangling References to Stack Frames [DCM]SPARK prevents this vulnerability. SPARK forbids the use of the ‘Address attribute to read the address of an object [SLRM 4.1]. The ‘Access attribute and all access types are also forbidden, so this vulnerability cannot occur. SPARK.36 Subprogram Signature Mismatch [OTR]SPARK mitigates this vulnerability. Default values for subprogram are not permitted in SPARK [SLRM 6], so this case cannot occur. SPARK does permit calling modules written in other languages so, as in Ada.36 [OTR], additional steps are required to verify the number and type-correctness of such parameters. SPARK also allows a subprogram body to be written in full-blown Ada (not SPARK). In this case, the subprogram body is said to be “hidden”, and no static analysis is performed by a SPARK Processor. For such hidden bodies, some alternative means of verification must be employed, and the advice of Annex Ada should be applied.
SPARK.37 Recursion [GDL]SPARK does not permit recursion, so this vulnerability is prevented [SLRM 6]. SPARK.38 Ignored Error Status and Unhandled Exceptions [OYB]SPARK mitigates this vulnerability. In SPARK, the normal approach is to use static analysis to prove that predefined exceptions cannot be raised. User-defined exceptions are not permitted. As recommended in Ada.38.2, it may be appropriate to retain a single “top-level” exception handler for each task as an additional defence. The vulnerability relating to an ignored error status is prevented by SPARK through static information flow analysis [IFA]. SPARK.39 Termination Strategy [REU]SPARK mitigates this vulnerability. SPARK permits a limited subset of Ada’s tasking facilities known as the “Ravenscar Profile” [SLRM 9]. There is no nesting of tasks in SPARK, and all tasks are required to have a top-level loop which has no exit statements, so this vulnerability does not apply in SPARK. SPARK is also amenable to static analysis for the absence of predefined exceptions [SB 11], thus mitigating the case where a task terminates prematurely (and silently) owing to an unhandled predefined exception.
SPARK.40 Type-breaking Reinterpretation of Data [AMV]SPARK mitigates this vulnerability. SPARK permits the instantiation and use of Unchecked_Conversion as in Ada. The result of a call to Unchecked_Conversion is not assumed to be valid, so static verification tools can then insist on re-validation of the result before further analysis can succeed [SB 11]. At the time of writing, SPARK does not permit discriminated records, so vulnerabilities relating to discriminated records and unchecked unions are prevented.
SPARK.41 Memory Leak [XYL]SPARK prevents this vulnerability. SPARK does not permit the use of access types, storage pools, or allocators, so this vulnerability cannot occur [SLRM 3]. In SPARK, all objects have a fixed size in memory, so the language is also amenable to static analysis of worst-case memory usage. SPARK.42 Templates and Generics [SYM]At the time of writing, SPARK does not permit the use of generics units, so this vulnerability is currently prevented. In future, the SPARK language may be extended to permit generic units, in which case section Ada.42 [SYM] applies. SPARK.43 Inheritance [RIP]SPARK mitigates this vulnerability. SPARK permits only a subset of Ada’s inheritance facilities to be used. Multiple inheritance, class-wide operations and dynamic dispatching are not permitted, so all vulnerabilities relating to these language features do not apply to SPARK [SLRM 3.8]. SPARK is also designed to be amenable to static verification of the Liskov Substitution Principle [LSP].
SPARK.44 Extra Intrinsics [LRM]SPARK prevents this vulnerability in the same way as Ada. See Ada.44 [LRM]. SPARK.45 Argument Passing to Library Functions [TRJ]SPARK mitigates this vulnerability. SPARK includes all of the mitigations of Ada with respect to this vulnerability, but goes further, allowing preconditions to be checked statically by a theorem-prover. The language in which such preconditions are expressed is also substantially more expressive than Ada’s type system. SPARK.46 Inter-language Calling [DJS]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.46 [DJS]. SPARK.47 Dynamically-linked Code and Self-modifying Code [NYY]SPARK prevents this vulnerability in the same way as Ada. See Ada.47 [NYY]. SPARK.48 Library Signature [NSQ]SPARK prevents this vulnerability in the same way as Ada. See Ada.48 [NSQ]. SPARK.49 Unanticipated Exceptions from Library Routines [HJW]SPARK prevents this vulnerability in the same way as Ada. See Ada.49 [HJW]. SPARK does permit the use of exception handlers, so these may be used to catch unexpected exceptions from library routines. SPARK.50 Pre-Processor Directives [NMP]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.50 [NMP]. SPARK.51 Suppression of Language-defined Run-time Checking [MXB]SPARK mitigates this vulnerability through static analysis. In particular, theorem-proving can be used to verify that a run-time check can never fail, allowing such checks to be suppressed with confidence [SB 11]. SPARK.52 Provision of Inherently Unsafe Operations [SKL]As in Ada, SPARK allows the use of Unchecked_Conversion, so the advice of Ada.52 applies here. SPARK allows provides a provision for “hidden” bodies – units not written in SPARK at all that are ignored by a SPARK Processor. These units are assumed to be written in Ada, so for these units, the advice of the entire Ada Annex should be applied. SPARK.53 Obscure Language Features [BRS]SPARK mitigates this vulnerability. The design of the SPARK subset avoids many language features that might be said to be “obscure” or “hard to understand”, such as controlled types, unrestricted tasking, anonymous access types and so on. SPARK goes further, though, in aiming for a completely unambiguous semantics, removing all erroneous and implementation-dependent features from the language. This means that a SPARK program should have a single meaning to programmers, reviewers, maintainers and all compilers. SPARK also bans the aliasing, overloading, and redeclaration of names, so that one entity only ever has one name and one name can denote at most one entity, further reducing the risk of mis-understanding or mis-interpretation of a program by a person, compiler or other tools. SPARK.54 Unspecified Behaviour [BQF]SPARK prevents this vulnerability. SPARK is designed to eliminate all unspecified language features and bounded errors, either by subsetting to make the offending language feature illegal in SPARK, or by ensuring that the language has neutral semantics with regard to an unspecified behaviour. “Neutral semantics” means that the program has identical meaning regardless of the choice made by a compiler for a particular unspecified language feature. For example:
SPARK.55 Undefined Behaviour [EWF]SPARK prevents this vulnerability through subsetting and static analysis. The language is designed to exhibit no undefined behaviours. SPARK.56 Implementation-Defined Behaviour [FAB]SPARK mitigates this vulnerability. SPARK allows a number of implementation-defined features as in Ada. These include:
In the first four cases, static analysis tools can be configured to “know” the appropriate values [SB 9.6]. Care must be taken to ensure that these values are correct for the intended implementation. In the fifth case, SPARK defines a contract to indicate the choice of base-type, which can be checked by a pragma Assert. In the final case, additional static analysis of numerical precision must be performed by the user to ensure the correctness of floating-point algorithms. SPARK.57 Deprecated Language Features [MEM]SPARK is identical to Ada with respect to this vulnerability and its mitigation. See Ada.57 [MEM]. SPARK.58 Implications for standardizationSee Ada.58. Yüklə 77 Kb. Dostları ilə paylaş:
|