Changeset 3634


Ignore:
Timestamp:
Mar 8, 2017, 11:01:45 AM (7 weeks ago)
Author:
mulligan
Message:

more fleshing out

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/introduction.tex

    r3633 r3634  
    1414Programs are specified using both functional and non-functional constraints.
    1515Functional constraints dictate what tasks a program must do; non-functional constraints limit the resources the program may consume whilst completing those tasks.
     16
    1617Depending on the application domain, non-functional constraints are as important as functional constraints when specifying a program.
    17 Real-time systems, with hard limits on application response times, and implementations of cryptographic primitives, which must be hardened to timing side-channel attacks, are two examples that fit this pattern.
     18Real-time systems, with hard limits on application response times, implementations of cryptographic primitives, which must be hardened to timing side-channel attacks, and a heart pacemaker's embedded controller, which must fit inside a limited code memory space, are examples that fit this pattern.
    1819A cryptography library susceptible to a timing side-channel attack is not an annoyance---it's an implementation error that undermines the entire purpose of the library.
     20
     21A program's non-functional constraints may be given \emph{concretely}, or \emph{asymptotically}.
     22Asymptotic complexity, as every Computer Science undergraduate knows, is important---but so too is concrete complexity for many applications, including the three we highlighted in our example above.
     23A real-time system's response time is measured in seconds, milliseconds, or some other fundamental unit of time; a cryptographic library must have all execution paths execute in the same number of processor cycles, independent of any input passed by the client; and the size of an embedded controller for a pacemaker is measured in bits, bytes, or some other unit of memory capacity.
    1924
    2025Currently, a program's functional properties can be established by combining user annotations---preconditions, invariants, and so on---with various automated and semi-automated analyses---invariant generators, type systems, abstract interpretations, applications of theorem proving, and so on---on the high-level source code of the program.
     
    3035The object code produced by an optimising compiler may have a radically different control flow to the original source code program.
    3136\item
    32 Object-code analysis is unstable.
     37Object code analysis is unstable.
    3338Modern compilers and linkers are highly non-compositional: they implement a variety of sophisticated optimisation passes, and use an abundance of procedural, intra-procedural, module-level, and link-time analyses to direct these optimisations.
    34 As a result, small changes in high-level source code can produce radically different object code outputs from a compiler, affecting any analysis effected on that object code.
     39As a result, small changes in high-level source code can produce radically different object code outputs from a compiler, affecting any analysis tied to that object code.
    3540\item
    3641It is well understood by Software Engineers that problems with the design or implementation of a program are cheaper to resolve early in the development process. %cite
    37 Despite this, techniques that operate on object code are not useful early in the development process of a program, where programs may be incomplete, with missing functionality, or entire subcomponents missing.
     42Despite this, techniques that operate on object code are not useful early in the development process of a program, where programs may be incomplete, with missing functionality, or missing modules.
    3843\item
    3944Parametric cost analysis is very hard: how can we translate a cost that depends on the execution state, for example the value of a register or a carry bit, to a cost that the user can understand whilst looking at the source code?
     
    145150hardware models.
    146151
    147 \subsection{Current object-code methods}
     152\subsection{Current object code methods}
    148153
    149154Analysis currently takes place on object code for two main reasons.
Note: See TracChangeset for help on using the changeset viewer.