MAIN DEFINITIONS OF VOCABULARY USED WITHIN THE PROJECT

A B C D F H I L M N O P R S T V

A

Access Property A quality characteristic describing the (declarative) policies for accessing a networked application. (Based on Sensoria glossary)

Accessibility A percentage of networked application responses per application requests. It can be measured by the number of successfully completed requests per application instantiations (i.e., completed application invocations). (Based on Sensoria glossary)

Attribute certificate A digital certificate that binds a set of descriptive data items, other than a public key, either directly to a subject name or to the identifier of another certificate that is a public-key certificate. In particular it may denote:

• "A set of attributes of a user together with some other information, rendered unforgeable by the digital signature created using the private key of the CA which issued it."
• "A data structure that includes some attribute values and identification information about the owner of the attribute certificate, all digitally signed by an Attribute Authority. This authority's signature serves as the guarantee of the binding between the attributes and their owner."

(Based on IETF Internet Security Glossary)

Authentication The process of validating the credentials of a person, service or device. Authentication requires the entity making the request to provide a credential that proves it is what or who it says is.
Common forms of credentials are user names and passwords, digital signatures, smart cards, etc. (Based on Sensoria glossary)

Authorization The process of granting a person, application or device access to certain protected information, services or functionality. Authorization is derived from the identity of the person, application or device making the request, which is verified through authentication. (Based on Sensoria glossary)

Availability The readiness of the networked application, i.e. the probability that the system is up and the service offered by an application provider is ready to be consumed by a service requester (where repair and downtimes of the system are considered) (QoS for Web Services). It can be measured by a ratio of the expected value of the uptime of a service to the aggregate of the expected values of up and down time. The number of successfully completed requests corresponds to Accessibility. (Based on Sensoria glossary)

B

Bytecode A binary representation of an executable program designed to be executed by a virtual machine rather than by dedicated hardware. This form of low-level programming language is often more abstract than machine code for hardware processors. Usually different units of the executable program are stored in separate files which are subsequently combined in a single software bundle associated with a particular application or software library.

C

Capability A token, usually an unforgeable data value (sometimes called a "ticket") that gives the bearer or holder the right to access a system resource. Possession of the token is accepted by a system as proof that the holder has been authorized to access the resource named or indicated by the token.
This concept can be implemented as a digital certificate. (See: attribute certificate.) (Based on IETF Internet Security Glossary)

Certifying compiler A compiler of a high-level programming language source code which aside the standard compilation to the machine code performs a transformation of a specified properties of the code and the proof that the code has the properties to a certificate which can be verified at the code consumer's site.

Certificate General English usage: A document that attests to the truth of something or the ownership of something. Security usage: See: capability, digital certificate.
PKI usage: See: attribute certificate, public-key certificate. (Based on IETF Internet Security Glossary)
In the context of MOBIUS it is an electronic document or data structure which incorporates a digital representation of a proof that a property associated with the certificate holds. Currently, the most typical kind of certificate is a certificate of identity based on the public key infrastructure. The proof-carrying code paradigm allows to define certificates that certify properties of the executable code associated with the certificate.

Certificate checker A hardware device or an application that is able to verify that a given certificate indeed certifies the assumed property.

Certificate issuer An entity (an organisation or an individual) who generates the certificate. It may be the code producer as well as a third party entity that specialises in certificate generation.

Certificate translation A process of transformation of a software certificate expressed in one format to another format. The process of translation may reduce the strength of the certificate i.e. the resulting certificate may certify a weaker property of the software.

Certification Information system usage: Technical evaluation (usually made in support of an accreditation action) of an information system's security features and other safeguards to establish the extent to which the system's design and implementation meet specified security requirements.
Digital certificate usage: The act or process of vouching for the truth and accuracy of the binding between data items in a certificate.
Public key usage: The act or process of vouching for the ownership of a public key by issuing a public-key certificate that binds the key to the name of the entity that possesses the matching private key. In addition to binding a key to a name, a public-key certificate may bind those items to other restrictive or explanatory data items.
SET usage: "The process of ascertaining that a set of requirements or criteria has been fulfilled and attesting to that fact to others, usually with some written instrument. A system that has been inspected and evaluated as fully compliant with the SET protocol by duly authorized parties and process would be said to have been certified compliant."

Code consumer An entity (an organisation or an individual) that runs the executable version of the code.

Code producer An entity (an organisation or an individual) that creates the source code or the executable code of an application. Typical code producer is a software company that creates an application. In some cases the production of the source code and the executable code may be separated e.g. when a big company outsources the software development, but it ships the final software bundle. In such cases the term code producer may mean depending on the context the software developer, the executable creator or even the whole compound entity that together does the development and the compilation.

Composition A way of fulfilling a business goal by means of a complex activity. The complex activity consists of a session that may involve operations that can be internal or performed by external participants. A composition can be achieved through programming languages (i.e., within the application code) or using a composition language (i.e., separating computation and coordination). (Based on Sensoria glossary)

Constraint A condition imposed on a software system by an external entity or the environment in which the software is to be run. The physical environment and the hardware architecture may impose constraints on the design of an operating system. The legal issues, the legacy software systems etc. may impose constraints on a particular software solution.

Confidentiality A property of a communication channel in which data is treated so that only authorized entities can access or modify the data. (Based on Sensoria glossary)

Coordination An execution-time activity that assures the mobile programs to act according on the agreed protocol. Coordination can be enacted by a component that is exposed as a service itself. (Based on Sensoria glossary)

D

Data encryption A process of converting data into coded form (cyphertext) to prevent it from being read or understood by an unauthorized party. (Based on Sensoria glossary)

Digital certificate A certificate document in the form of a digital data object (a data object used by a computer) to which is appended a computed digital signature value that depends on the data object.
Documents SHOULD NOT use this term to refer to a signed CRL or CKL. Although the recommended definition can be interpreted to include those items, the security community does not use the term with those meanings.
The proof-carrying code paradigm allows to define certificates that certify properties of the executable code associated with the certificate. (Based on IETF Internet Security Glossary)

Dynamic checking see Run-time checking

F

Functional correctness A program is functionally correct when it has all its designated functional properties.

Functional Description A description of a mobile program which includes

• the semantics of the program,
• the interface of the program,
• the abstract set of scenarios to describe the interactive behaviour of the program.

(Based on Sensoria glossary)

H

Hybrid certificate A kind of the proof-carrying code certificate which is based on both the properties of the executable code expressible in type systems and in program logics.

I

Integrity A property of a networked application due to which a system or component can prevent unauthorized access to, or modification of, computer programs or data. There can be two types of integrity: data integrity and transactional integrity. (QoS for Web Services)

• Data integrity defines whether the transferred data is modified in transit (see also the definitions of Security).
• Transactional integrity refers to a procedure or set of procedures, which is guaranteed to preserve database integrity in a transaction (see Transactionality).
  

Often the term integrity is referred to by explicitly indicating the sense (e.g. in "Integrity w.r.t. a particular characteristic"). For example: integrity w.r.t safety is defined as: The likelihood of a system satisfactorily performing the required safety functions under all the stated conditions within a stated period of time.
(Based on Sensoria glossary)

Intermediary An entity (an organisation or an individual) that mediates in the chain of software delivery between the code producer and the code consumer. The chain of software delivery may consist of several intermediaries e.g. ISP of the code producer, ISP of the mobile phone network provider, the mobile phone network provider.

L

Logic based certificate A proof-carrying code certificate which is based on the properties of the executable code expressible in program logics.

M

Mobile code Software obtained from remote systems, transferred across a network, and then downloaded and executed on a local system. It may but need not require explicit installation or execution by the recipient.

N

Non-functional Description A description which is built from a number of non-functional properties. It involves the enumeration of properties seen from a coarse grained perspective. For example, we consider the enumeration of which kind of transactional support a mobile code can provide as non-functional. When the focus shifts on how this support is provided, as in the case of compensating transactions (they can be undone but only in a certain measure), then the matter becomes functional as their semantics depend on the semantics of their compensations and by their usage within a composed actvity. (Based on Sensoria glossary)

Non-functional Property A property that does not affect the meaning of the provided service and that describes a feature of a service by ignoring the details of how the property is provided. It is a statement (e.g., the couple attribute = value) involving an attrbute, characterized by a non-functional datatype, that can assume different values in time during the runtime execution of a service (i.e., runtime values). (Based on Sensoria glossary)

Non-repudiation A method by which the sender of data is provided with proof of delivery and the recipient is assured of the sender's identity, so that neither can later deny having processed the data. (Based on Sensoria glossary and W3C Glossary)

O

On-device verifier A software verifier that operates on the device which will execute the verified software.

Off-device verifier A software verifier that operates on a machine which will not execute the verified software.

P

Policy A description which defines a desirable property of a computer system. Policies are enforced by

• the way the system is implemented,
• the way the system interacts with its environment,
• the way the system interacts with its users.

Postcondition A condition that must be true after a particular piece of software has been executed. (Based on Sensoria glossary)

Precondition A condition that must be true in order to enable the execution of a particular piece of software. (Based on Sensoria glossary)

Proof A demonstration that, assuming certain axioms, some statement is necessarily true. A proof is a logical argument, not an empirical one. In software verification, it is sometimes understood as a digital representation of the argument in a particular proof generation environment.

Proof-carrying code (PCC) An additional mechanism that allows a system that runs a software application to verify its properties by means of a formal proof shipped together with the application's executable code. The host system can check if the properties imply its own security policy to determine whether the application is safe to execute. This can be particularly useful in preventing the software vulnerabilities.

Property A quality of software or its component which describes its certain capability. The properties determine the usability of the software. The properties may be functional (i.e. the ones that determine the meaning of the component, for example the results obtained for given arguments) and non-functional (i.e. the ones that are independent of the meaning of the component, for example the technology in which the particular functionality is realized).

Public-key certificate A digital certificate that binds a system entity's identity to a public key value, and possibly to additional data items; a digitally-signed data structure that attests to the ownership of a public key.
The digital signature on a public-key certificate is unforgeable. Thus, the certificate can be published, such as by posting it in a directory, without the directory having to protect the certificate's data integrity. (Based on IETF Internet Security Glossary)

Public Key Infrastructure (PKI) An arrangement that corelates public keys with particular user identities. It is usually accomplished by means of a certificate authority (CA). The CA ensures that the electronical identity is associated with the actual person or organisation. This is carried out by software at a CA, possibly under human supervision, together with other coordinated software at distributed locations. The certificates issued by the CA are arranged so that the user identity, the public key, their binding, validity conditions and other attributes are unforgeable. Aother form of PKI is based on the so called web of trust which uses self-signed certificates and third party attestations of those certificates to ensure their authenticity.

R

Requirement A property of a software system which identifies an attribute, capability, behaviour, characteristic, or quality of the software. In a typical software development the software requirement is documented at the stage of the problem analysis and further realised at the stage of the software development.

Resource (or system resource) Any physical or virtual component of limited availability within a computer system. Every device connected to a computer system is a resource. Every internal system component is a resource. Virtual system resources include files, network connections and memory areas. (Wikipedia)

Rights Rights refers to information about rights held in and over the element. Typically, rights will contain a rights management statement for the element or reference a service providing such information. Rights information often encompasses Intellectual Property Rights (IPR), copyright, and various property rights. If the rights element is absent, no assumptions may be made about any rights held in or over the element. (Based on Sensoria glossary)

Rule This word has several meanings depending on the context. (i) In case of logical or typing systems, the word "rule" is used as an inference rule i.e. a concise description of which requirements must be fulfilled in order to make the final statement hold. (ii) In case of a list of generic requirements, the word "rule" is used to denote one of generic requirements that can be used for a particular piece of software.

Run-time checking A process to verify that an executable code has certain property. The verification is done by running the actual program and checking in the course of the execution that the intended properties hold. This is done by execution of special guard code which checks the expected properties.

S

Safety A user-oriented quality requirement that specifies the degree to which a mobile application shall not directly or indirectly (e.g. via inactivity) cause accidental harm to either life (e.g., injury, loss of life) or property (e.g., loss of money or corruption of valuable data).
The safety requirement for a mobile application is defined in conjunction with the artefacts the application interacts with, for example: the safety requirement for an application that places an automated phone call to the drivers mobile phone in case of a deployed airbag must provide the ability to block all other incoming phone calls. (Based on Sensoria glossary)

Scenario A description of foreseeable interactions between the predicted types of users and a software system or between two or more software components. Scenarios usually include information about goals, expectations, actions and reactions. In MOBIUS, the scenarios describe possible ways the proof-carrying code traverses between the code originator and the code consumer. The scenarios may involve: several code consumers, several code producers, and intermediaries.

Security The ability of a piece of software to provide

• Authentication
• Authorization
• Confidentiality
• Traceability/auditability
• Data encryption
• Non-repudiation

(Based on Sensoria glossary)

Session A lasting interaction between system entities, often involving a user, typified by the maintenance of some state of the interaction for the duration of the interaction W3C Web Service Glossary. A number of session capabilities may characterize a session, such as

• Duration (how long a session can last)
• Access rights
• Number of allowed service invocations during a session
• Ownership of a session
• Order of invocations

(Based on Sensoria glossary)

Software certification entity An organisation or a person that prepares a digital certificate. A particular case of the software certification entity is a certification authority that issues public-key certificate. In case of the PCC certificates, a software certification entity is an organisation or a person that prepares the specification of a program code and a proof that the code has the specified property.

Software verifier A program or a system which verifies with the use of mathematical standards and methodologies that a particular piece of software has indicated properties.

Static verification A process of verification of a program property which is performed at the time of the program compilationn

Statefulness A property of a piece of software which means that a running instance of a mobile program takes into account in operation the history of previous events the program took part in. (Based on Sensoria glossary)

T

Traceability/auditability A property of a piece of software which ensures that it should be possible to log the history of a mobile application when a request was placed. (Based on Sensoria glossary)

Transactionality It represents the transactional properties of the operation. A transactional operation can be committed in the case of success, otherwise it is rolled back. In the context of long running transactions - where the resources cannot be accessed exclusively during the transaction - transactions are managed by fault handling or compensation actions.
Traditionally, requirements against a transactional service can be:

• Atomicity: Either the entire transaction is executed or none of the steps of the transactional sequence.
• Consistency: The system is in a consistent state after the execution of the transaction.
• Isolation: All parallel transactions are executed as there were only one transaction in the system.
• Durability: The result of a transaction is persistent.
  

(Based on Sensoria glossary)

Trusted computing base (TCB) A set of computer system elements which includes all the hardware, firmware, and/or software components that are critical to the security of a particular application or computing environment. The bugs in the TCB may lead to security breaches in the application or environment. It is assumed that the TCB is of small size so that it is amenable to exhaustive security analysis. The parts of a computer system outside the TCB supposedly can misbehave without affecting security.

Trusted intermediary A network intermediary who provides certain level of assurance with regard to some safety property concerning the mobile code. In particular, an intermediary who guarantees that the mobile code stays intact while in his hands is already a trusted intermediary. A trusted intermediary may also guarantee stronger properties such as the mobile code which comes out of his hands is guaranteed not to send more than 10 SMS's each time it is run.

Trustworthiness The assurance that a system deserves to be trusted-that it will perform as expected despite environmental disruptions, human and operator error, hostile attacks, and design and implementation errors. Trustworthy systems reinforce the belief that they will continue to produce expected behavior and will not be susceptible to subversion. (Based on Sensoria glossary and Committee on Information Systems Trustworthiness)

Type based certificate A proof-carrying code certificate which is based on the properties of the executable code expressible in type systems.

V

Validate vs. verify The PKI community uses words inconsistently when describing what a certificate user does to make certain that a digital certificate can be trusted. Usually, we say "verify the signature" but say "validate the certificate"; i.e., we "verify" atomic truths but "validate" data structures, relationships, and systems that are composed of or depend on verified items. Too often, however, verify and validate are used interchangeably.
Documents SHOULD comply with the following two rules to ensure consistency and to align Internet security terminology with ordinary English:

• Rule 1: Use "validate" when referring to a process intended to establish the soundness or correctness of a construct. (E.g., see: certificate validation.)
• Rule 2: Use "verify" when referring to a process intended to test or prove the truth or accuracy of a fact or value. (E.g., see: authenticate.)
  

The rationale for Rule 1 is that "valid" derives from a word that means "strong" in Latin. Thus, to validate means to make sure that a construction is sound. A certificate user validates a public-key certificate to establish trust in the binding that the certificate asserts between an identity and a key. (To validate can also mean to officially approve something; e.g., NIST validates cryptographic modules for conformance with FIPS PUB 140-1.)
The rationale for Rule 2 is that "verify" derives from a word that means "true" in Latin. Thus, to verify means to prove the truth of an assertion by examining evidence or performing tests. To verify an identity, an authentication process examines identification information that is presented or generated. To validate a certificate, a certificate user verifies the digital signature on the certificate by performing calculations; verifies that the current time is within the certificate's validity period; and may need to validate a certification path involving additional certificates. (Based on IETF Internet Security Glossary)

Verification condition A condition that is an obligation to be proved in order to obtain a particular desired property of a program. Verification condidions are usually automatically generated based upon specifications that describe the desired program property.

Verification protocol A protocol which ensures that a particular property of a program is verified.

Virtual machine A piece of computer software that executes a user application and isolates it from the actual processing system (i.e. operating system and hardware). Usually a virtual machine is written for various platforms, so any application written for the virtual machine can be operated on any of the platforms. The application is run on the computer using an interpreter or Just In Time compilation.