enforcing shorter Definition* - style in examples (CC,CENELEC,...)
This commit is contained in:
parent
8771d8581b
commit
0e64608a58
|
@ -16,6 +16,8 @@ theory "00_Frontmatter"
|
|||
imports "Isabelle_DOF.technical_report"
|
||||
begin
|
||||
|
||||
text\<open> \<open> \<tau>\<close>\<close>
|
||||
|
||||
section\<open>Document Local Setup.\<close>
|
||||
text\<open>Some internal setup, introducing document specific abbreviations and macros.\<close>
|
||||
|
||||
|
|
|
@ -702,7 +702,7 @@ proof - fix a :: nat
|
|||
|
||||
subsection*[t233::technical]\<open> Theories and the Signature API\<close>
|
||||
text\<open>
|
||||
\<^enum> \<^ML>\<open>Sign.tsig_of : theory -> Type.tsig\<close> extraxts the type-signature of a theory
|
||||
\<^enum> \<^ML>\<open>Sign.tsig_of : theory -> Type.tsig\<close> extracts the type-signature of a theory
|
||||
\<^enum> \<^ML>\<open>Sign.syn_of : theory -> Syntax.syntax\<close> extracts the constant-symbol signature
|
||||
\<^enum> \<^ML>\<open>Sign.of_sort : theory -> typ * sort -> bool\<close> decides that a type belongs to a sort.
|
||||
\<close>
|
||||
|
|
|
@ -10,7 +10,7 @@ begin
|
|||
text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for
|
||||
semi-formal terminology, which we re-use by this definition.\<close>
|
||||
|
||||
doc_class concept_definition = "definition" +
|
||||
doc_class concept_definition = math_content +
|
||||
status :: status <= "semiformal"
|
||||
mcc :: math_content_class <= "terminology"
|
||||
tag :: string
|
||||
|
@ -20,6 +20,9 @@ text\<open>The \<^verbatim>\<open>short_tag\<close>, if set, is used in the pres
|
|||
|
||||
type_synonym concept = concept_definition
|
||||
|
||||
declare[[ Definition_default_class="concept_definition"]]
|
||||
|
||||
|
||||
(*>>*)
|
||||
|
||||
section \<open>Terminology\<close>
|
||||
|
@ -27,86 +30,86 @@ section \<open>Terminology\<close>
|
|||
|
||||
subsection \<open>Terms and definitions common in the CC\<close>
|
||||
|
||||
Definition* [aas_def::concept, tag= "''adverse actions''"]
|
||||
Definition* [aas_def, tag= "''adverse actions''"]
|
||||
\<open>actions performed by a threat agent on an asset\<close>
|
||||
|
||||
declare_reference*[toe_def::concept]
|
||||
declare_reference*[toe_def]
|
||||
|
||||
Definition* [assts_def::concept, tag="''assets''"]
|
||||
Definition* [assts_def, tag="''assets''"]
|
||||
\<open>entities that the owner of the @{docitem toe_def} presumably places value upon \<close>
|
||||
|
||||
Definition* [asgn_def::concept, tag="''assignment''"]
|
||||
Definition* [asgn_def, tag="''assignment''"]
|
||||
\<open>the specification of an identified parameter in a component (of the CC) or requirement.\<close>
|
||||
|
||||
declare_reference*[sfrs_def::concept]
|
||||
declare_reference*[sfrs_def]
|
||||
|
||||
Definition* [assrc_def::concept, tag="''assurance''"]
|
||||
Definition* [assrc_def, tag="''assurance''"]
|
||||
\<open>grounds for confidence that a @{docitem toe_def} meets the @{docitem sfrs_def}\<close>
|
||||
|
||||
Definition* [attptl_def::concept, tag="''attack potential''"]
|
||||
Definition* [attptl_def, tag="''attack potential''"]
|
||||
\<open>measure of the effort to be expended in attacking a TOE, expressed in terms of
|
||||
an attacker's expertise, resources and motivation\<close>
|
||||
|
||||
Definition* [argmt_def::concept, tag= "''augmentation''"]
|
||||
Definition* [argmt_def, tag= "''augmentation''"]
|
||||
\<open>addition of one or more requirement(s) to a package\<close>
|
||||
|
||||
Definition* [authdata_def::concept, tag="''authentication data''"]
|
||||
Definition* [authdata_def, tag="''authentication data''"]
|
||||
\<open>information used to verify the claimed identity of a user\<close>
|
||||
|
||||
Definition* [authusr_def::concept, tag = "''authorised user''"]
|
||||
Definition* [authusr_def, tag = "''authorised user''"]
|
||||
\<open>@{docitem toe_def} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\<close>
|
||||
|
||||
Definition* [bpp_def::concept, tag="''Base Protection Profile''"]
|
||||
Definition* [bpp_def, tag="''Base Protection Profile''"]
|
||||
\<open>Protection Profile used as a basis to build a Protection Profile Configuration\<close>
|
||||
|
||||
Definition* [cls_def::concept,tag="''class''"]
|
||||
Definition* [cls_def,tag="''class''"]
|
||||
\<open>set of CC families that share a common focus\<close>
|
||||
|
||||
Definition* [cohrnt_def::concept,tag="''coherent''"]
|
||||
Definition* [cohrnt_def,tag="''coherent''"]
|
||||
\<open>logically ordered and having discernible meaning For documentation, this addresses
|
||||
both the actual text and the structure of the document, in terms of whether it is
|
||||
understandable by its target audience.\<close>
|
||||
|
||||
Definition* [cmplt_def::concept, tag="''complete''"]
|
||||
Definition* [cmplt_def, tag="''complete''"]
|
||||
\<open>property where all necessary parts of an entity have been provided
|
||||
In terms of documentation, this means that all relevant information is
|
||||
covered in the documentation, at such a level of detail that no further
|
||||
explanation is required at that level of abstraction.\<close>
|
||||
|
||||
Definition* [compnt_def::concept, tag="''component''"]
|
||||
Definition* [compnt_def, tag="''component''"]
|
||||
\<open>smallest selectable set of elements on which requirements may be based\<close>
|
||||
|
||||
Definition*[cap_def::concept, tag="''composed assurance package''"]
|
||||
Definition*[cap_def, tag="''composed assurance package''"]
|
||||
\<open>assurance package consisting of requirements drawn from CC Part 3
|
||||
(predominately from the ACO class), representing a point on the CC predefined
|
||||
composition assurance scale\<close>
|
||||
|
||||
Definition* [cfrm_def::concept,tag="''confirm''"]
|
||||
Definition* [cfrm_def,tag="''confirm''"]
|
||||
\<open>declare that something has been reviewed in detail with an independent determination
|
||||
of sufficiency
|
||||
|
||||
The level of rigour required depends on the nature of the subject matter. This
|
||||
term is only applied to evaluator actions.\<close>
|
||||
|
||||
Definition* [cnnctvty_def::concept, tag="''connectivity''"]
|
||||
Definition* [cnnctvty_def, tag="''connectivity''"]
|
||||
\<open>property of the @{docitem toe_def} allowing interaction with IT entities external to the
|
||||
@{docitem toe_def}
|
||||
|
||||
This includes exchange of data by wire or by wireless means, over any
|
||||
distance in any environment or configuration.\<close>
|
||||
|
||||
Definition* [cnstnt_def::concept, tag="''consistent''"]
|
||||
Definition* [cnstnt_def, tag="''consistent''"]
|
||||
\<open>relationship between two or more entities such that there are no apparent
|
||||
contradictions between these entities\<close>
|
||||
|
||||
Definition* [cnt_vrb_def::concept, tag="''counter, verb''"]
|
||||
Definition* [cnt_vrb_def, tag="''counter, verb''"]
|
||||
\<open>meet an attack where the impact of a particular threat is mitigated
|
||||
but not necessarily eradicated\<close>
|
||||
|
||||
declare_reference*[st_def::concept]
|
||||
declare_reference*[pp_def::concept]
|
||||
declare_reference*[st_def]
|
||||
declare_reference*[pp_def]
|
||||
|
||||
Definition* [dmnst_conf_def::concept, tag="''demonstrable conformance''"]
|
||||
Definition* [dmnst_conf_def, tag="''demonstrable conformance''"]
|
||||
\<open>relation between an @{docitem st_def} and a @{docitem pp_def}, where the @{docitem st_def}
|
||||
provides a solution which solves the generic security problem in the PP
|
||||
|
||||
|
@ -116,19 +119,19 @@ also suitable for a @{docitem toe_def} type where several similar @{docitem pp_d
|
|||
allowing the ST author to claim conformance to these @{docitem pp_def}s simultaneously,
|
||||
thereby saving work.\<close>
|
||||
|
||||
Definition* [dmstrt_def::concept, tag="''demonstrate''"]
|
||||
Definition* [dmstrt_def, tag="''demonstrate''"]
|
||||
\<open>provide a conclusion gained by an analysis which is less rigorous than a “proof”\<close>
|
||||
|
||||
Definition* [dpndcy::concept, tag="''dependency''"]
|
||||
Definition* [dpndcy, tag="''dependency''"]
|
||||
\<open>relationship between components such that if a requirement based on the depending
|
||||
component is included in a @{docitem pp_def}, ST or package, a requirement based on
|
||||
the component that is depended upon must normally also be included in the @{docitem pp_def},
|
||||
@{docitem st_def} or package\<close>
|
||||
|
||||
Definition* [dscrb_def::concept, tag="''describe''"]
|
||||
Definition* [dscrb_def, tag="''describe''"]
|
||||
\<open>provide specific details of an entity\<close>
|
||||
|
||||
Definition* [dtrmn_def::concept, tag="''determine''"]
|
||||
Definition* [dtrmn_def, tag="''determine''"]
|
||||
\<open>affirm a particular conclusion based on independent analysis with the objective
|
||||
of reaching a particular conclusion
|
||||
|
||||
|
@ -137,35 +140,35 @@ Definition* [dtrmn_def::concept, tag="''determine''"]
|
|||
terms “confirm” or “verify” which imply that an analysis has already been
|
||||
performed which needs to be reviewed\<close>
|
||||
|
||||
Definition* [devenv_def::concept, tag="''development environment''"]
|
||||
Definition* [devenv_def, tag="''development environment''"]
|
||||
\<open>environment in which the @{docitem toe_def} is developed\<close>
|
||||
|
||||
Definition* [elmnt_def::concept, tag="''element''"]
|
||||
Definition* [elmnt_def, tag="''element''"]
|
||||
\<open>indivisible statement of a security need\<close>
|
||||
|
||||
Definition* [ensr_def::concept, tag="''ensure''"]
|
||||
Definition* [ensr_def, tag="''ensure''"]
|
||||
\<open>guarantee a strong causal relationship between an action and its consequences
|
||||
|
||||
When this term is preceded by the word “help” it indicates that the
|
||||
consequence is not fully certain, on the basis of that action alone.\<close>
|
||||
|
||||
Definition* [eval_def::concept, tag="''evaluation''"]
|
||||
Definition* [eval_def, tag="''evaluation''"]
|
||||
\<open>assessment of a @{docitem pp_def}, an @{docitem st_def} or a @{docitem toe_def},
|
||||
against defined criteria.\<close>
|
||||
|
||||
Definition* [eal_def::concept, tag= "''evaluation assurance level''"]
|
||||
Definition* [eal_def, tag= "''evaluation assurance level''"]
|
||||
\<open>set of assurance requirements drawn from CC Part 3, representing a point on the
|
||||
CC predefined assurance scale, that form an assurance package\<close>
|
||||
|
||||
Definition* [eval_auth_def::concept, tag="''evaluation authority''"]
|
||||
Definition* [eval_auth_def, tag="''evaluation authority''"]
|
||||
\<open>body that sets the standards and monitors the quality of evaluations conducted by bodies within a specific community and
|
||||
implements the CC for that community by means of an evaluation scheme\<close>
|
||||
|
||||
Definition* [eval_schm_def::concept, tag="''evaluation scheme''"]
|
||||
Definition* [eval_schm_def, tag="''evaluation scheme''"]
|
||||
\<open>administrative and regulatory framework under which the CC is applied by an
|
||||
evaluation authority within a specific community\<close>
|
||||
|
||||
Definition* [exst_def::concept, tag="''exhaustive''"]
|
||||
Definition* [exst_def, tag="''exhaustive''"]
|
||||
\<open>characteristic of a methodical approach taken to perform an
|
||||
analysis or activity according to an unambiguous plan
|
||||
This term is used in the CC with respect to conducting an analysis or other
|
||||
|
@ -175,31 +178,31 @@ analysis or activity according to an unambiguous plan, but that the plan that
|
|||
was followed is sufficient to ensure that all possible avenues have been
|
||||
exercised.\<close>
|
||||
|
||||
Definition* [expln_def::concept, tag="''explain''"]
|
||||
Definition* [expln_def, tag="''explain''"]
|
||||
\<open> give argument accounting for the reason for taking a course of action
|
||||
This term differs from both “describe” and “demonstrate”. It is intended to
|
||||
answer the question “Why?” without actually attempting to argue that the
|
||||
course of action that was taken was necessarily optimal.\<close>
|
||||
|
||||
Definition* [extn_def::concept, tag= "''extension''"]
|
||||
Definition* [extn_def, tag= "''extension''"]
|
||||
\<open>addition to an ST or PP of functional requirements not contained in CC
|
||||
Part 2 and/or assurance requirements not contained in CC Part 3\<close>
|
||||
|
||||
Definition* [extnl_ent_def::concept, tag="''external entity''"]
|
||||
Definition* [extnl_ent_def, tag="''external entity''"]
|
||||
\<open>human or IT entity possibly interacting with the TOE from outside of the TOE boundary\<close>
|
||||
|
||||
Definition* [fmly_def::concept, tag="''family''"]
|
||||
Definition* [fmly_def, tag="''family''"]
|
||||
\<open>set of components that share a similar goal but differ in emphasis or rigour\<close>
|
||||
|
||||
Definition* [fml_def::concept, tag="''formal''"]
|
||||
Definition* [fml_def, tag="''formal''"]
|
||||
\<open>expressed in a restricted syntax language with defined semantics
|
||||
based on well-established mathematical concepts \<close>
|
||||
|
||||
Definition* [gudn_doc_def::concept, tag="''guidance documentation''"]
|
||||
Definition* [gudn_doc_def, tag="''guidance documentation''"]
|
||||
\<open>documentation that describes the delivery, preparation, operation,
|
||||
management and/or use of the TOE\<close>
|
||||
|
||||
Definition* [ident_def::concept, tag="''identity''"]
|
||||
Definition* [ident_def, tag="''identity''"]
|
||||
\<open>representation uniquely identifying entities (e.g. a user, a process or a disk)
|
||||
within the context of the TOE
|
||||
|
||||
|
@ -207,110 +210,110 @@ Definition* [ident_def::concept, tag="''identity''"]
|
|||
representation can be the full or abbreviated name or a (still unique)
|
||||
pseudonym.\<close>
|
||||
|
||||
Definition* [infml_def::concept, tag="''informal''"]
|
||||
Definition* [infml_def, tag="''informal''"]
|
||||
\<open>expressed in natural language\<close>
|
||||
|
||||
Definition* [intr_tsf_trans_def::concept, tag ="''inter TSF transfers''"]
|
||||
Definition* [intr_tsf_trans_def, tag ="''inter TSF transfers''"]
|
||||
\<open>communicating data between the TOE and the security functionality of
|
||||
other trusted IT products\<close>
|
||||
|
||||
Definition* [intl_com_chan_def::concept, tag ="''internal communication channel''"]
|
||||
Definition* [intl_com_chan_def, tag ="''internal communication channel''"]
|
||||
\<open>communication channel between separated parts of the TOE\<close>
|
||||
|
||||
Definition* [int_toe_trans::concept, tag="''internal TOE transfer''"]
|
||||
Definition* [int_toe_trans, tag="''internal TOE transfer''"]
|
||||
\<open>communicating data between separated parts of the TOE\<close>
|
||||
|
||||
Definition* [inter_consist_def::concept, tag="''internally consistent''"]
|
||||
Definition* [inter_consist_def, tag="''internally consistent''"]
|
||||
\<open>no apparent contradictions exist between any aspects of an entity
|
||||
|
||||
In terms of documentation, this means that there can be no statements within
|
||||
the documentation that can be taken to contradict each other.\<close>
|
||||
|
||||
Definition* [iter_def::concept, tag="''iteration''"]
|
||||
Definition* [iter_def, tag="''iteration''"]
|
||||
\<open>use of the same component to express two or more distinct requirements\<close>
|
||||
|
||||
Definition* [jstfct_def::concept, tag="''justification''"]
|
||||
Definition* [jstfct_def, tag="''justification''"]
|
||||
\<open>analysis leading to a conclusion “Justification” is more rigorous than a demonstration.
|
||||
This term requires significant rigour in terms of very carefully and thoroughly explaining every
|
||||
step of a logical argument.\<close>
|
||||
|
||||
Definition* [objct_def::concept, tag="''object''"]
|
||||
Definition* [objct_def, tag="''object''"]
|
||||
\<open>passive entity in the TOE, that contains or receives information,
|
||||
and upon which subjects perform operations\<close>
|
||||
|
||||
Definition* [op_cc_cmpnt_def::concept, tag ="''operation (on a component of the CC)''"]
|
||||
Definition* [op_cc_cmpnt_def, tag ="''operation (on a component of the CC)''"]
|
||||
\<open>modification or repetition of a component
|
||||
Allowed operations on components are assignment, iteration, refinement and
|
||||
selection.\<close>
|
||||
|
||||
Definition* [op_obj_def::concept, tag= "''operation (on an object)''"]
|
||||
Definition* [op_obj_def, tag= "''operation (on an object)''"]
|
||||
\<open>specific type of action performed by a subject on an object\<close>
|
||||
|
||||
Definition* [op_env_def::concept, tag= "''operational environment''"]
|
||||
Definition* [op_env_def, tag= "''operational environment''"]
|
||||
\<open>environment in which the TOE is operated\<close>
|
||||
|
||||
Definition* [org_sec_po_def::concept, tag="''organisational security policy''"]
|
||||
Definition* [org_sec_po_def, tag="''organisational security policy''"]
|
||||
\<open>set of security rules, procedures, or guidelines for an organisation
|
||||
A policy may pertain to a specific operational environment.\<close>
|
||||
|
||||
Definition* [pckg_def::concept, tag="''package''"]
|
||||
Definition* [pckg_def, tag="''package''"]
|
||||
\<open>named set of either security functional or security assurance requirements
|
||||
An example of a package is “EAL 3”.\<close>
|
||||
|
||||
Definition* [pp_config_def::concept, tag="''Protection Profile Configuration''"]
|
||||
Definition* [pp_config_def, tag="''Protection Profile Configuration''"]
|
||||
\<open>Protection Profile composed of Base Protection Profiles and Protection Profile Module\<close>
|
||||
|
||||
Definition* [pp_eval_def::concept, tag="''Protection Profile evaluation''"]
|
||||
Definition* [pp_eval_def, tag="''Protection Profile evaluation''"]
|
||||
\<open> assessment of a PP against defined criteria \<close>
|
||||
|
||||
Definition* [pp_def::concept, tag="''Protection Profile''"]
|
||||
Definition* [pp_def, tag="''Protection Profile''"]
|
||||
\<open>implementation-independent statement of security needs for a TOE type\<close>
|
||||
|
||||
Definition* [ppm_def::concept, tag="''Protection Profile Module''"]
|
||||
Definition* [ppm_def, tag="''Protection Profile Module''"]
|
||||
\<open>implementation-independent statement of security needs for a TOE type
|
||||
complementary to one or more Base Protection Profiles\<close>
|
||||
|
||||
declare_reference*[tsf_def::concept]
|
||||
declare_reference*[tsf_def]
|
||||
|
||||
Definition* [prv_def::concept, tag="''prove''"]
|
||||
Definition* [prv_def, tag="''prove''"]
|
||||
\<open>show correspondence by formal analysis in its mathematical sense
|
||||
It is completely rigorous in all ways. Typically, “prove” is used when there is
|
||||
a desire to show correspondence between two @{docitem tsf_def} representations at a high
|
||||
level of rigour.\<close>
|
||||
|
||||
Definition* [ref_def::concept, tag="''refinement''"]
|
||||
Definition* [ref_def, tag="''refinement''"]
|
||||
\<open>addition of details to a component\<close>
|
||||
|
||||
Definition* [role_def::concept, tag="''role''"]
|
||||
Definition* [role_def, tag="''role''"]
|
||||
\<open>predefined set of rules establishing the allowed interactions between
|
||||
a user and the @{docitem toe_def}\<close>
|
||||
|
||||
declare_reference*[sfp_def::concept]
|
||||
declare_reference*[sfp_def]
|
||||
|
||||
Definition* [scrt_def::concept, tag="''secret''"]
|
||||
Definition* [scrt_def, tag="''secret''"]
|
||||
\<open>information that must be known only to authorised users and/or the
|
||||
@{docitem tsf_def} in order to enforce a specific @{docitem sfp_def}\<close>
|
||||
|
||||
declare_reference*[sfr_def::concept]
|
||||
declare_reference*[sfr_def]
|
||||
|
||||
Definition* [sec_st_def::concept, tag="''secure state''"]
|
||||
Definition* [sec_st_def, tag="''secure state''"]
|
||||
\<open>state in which the @{docitem tsf_def} data are consistent and the @{docitem tsf_def}
|
||||
continues correct enforcement of the @{docitem sfr_def}s\<close>
|
||||
|
||||
Definition* [sec_att_def::concept, tag="''security attribute''"]
|
||||
Definition* [sec_att_def, tag="''security attribute''"]
|
||||
\<open>property of subjects, users (including external IT products), objects,
|
||||
information, sessions and/or resources that is used in defining the @{docitem sfr_def}s
|
||||
and whose values are used in enforcing the @{docitem sfr_def}s\<close>
|
||||
|
||||
Definition* [sec_def::concept, tag="''security''"]
|
||||
Definition* [sec_def, tag="''security''"]
|
||||
\<open>function policy set of rules describing specific security behaviour enforced
|
||||
by the @{docitem tsf_def} and expressible as a set of @{docitem sfr_def}s\<close>
|
||||
|
||||
Definition* [sec_obj_def::concept, tag="''security objective''"]
|
||||
Definition* [sec_obj_def, tag="''security objective''"]
|
||||
\<open>statement of an intent to counter identified threats and/or satisfy identified
|
||||
organisation security policies and/or assumptions\<close>
|
||||
|
||||
Definition* [sec_prob_def::concept, tag ="''security problem''"]
|
||||
Definition* [sec_prob_def, tag ="''security problem''"]
|
||||
\<open>statement which in a formal manner defines the nature and scope of the security that
|
||||
the TOE is intended to address This statement consists of a combination of:
|
||||
\begin{itemize}
|
||||
|
@ -319,23 +322,23 @@ the TOE is intended to address This statement consists of a combination of:
|
|||
\item the assumptions that are upheld for the operational environment of the TOE.
|
||||
\end{itemize}\<close>
|
||||
|
||||
Definition* [sr_def::concept, tag="''security requirement''", short_tag="Some(''SR'')"]
|
||||
Definition* [sr_def, tag="''security requirement''", short_tag="Some(''SR'')"]
|
||||
\<open>requirement, stated in a standardised language, which is meant to contribute
|
||||
to achieving the security objectives for a TOE\<close>
|
||||
text \<open>@{docitem toe_def}\<close>
|
||||
Definition* [st::concept, tag="''Security Target''", short_tag="Some(''ST'')"]
|
||||
Definition* [st, tag="''Security Target''", short_tag="Some(''ST'')"]
|
||||
\<open>implementation-dependent statement of security needs for a specific i\<section>dentified @{docitem toe_def}\<close>
|
||||
|
||||
Definition* [slct_def::concept, tag="''selection''"]
|
||||
Definition* [slct_def, tag="''selection''"]
|
||||
\<open>specification of one or more items from a list in a component\<close>
|
||||
|
||||
Definition* [smfrml_def::concept, tag="''semiformal''"]
|
||||
Definition* [smfrml_def, tag="''semiformal''"]
|
||||
\<open>expressed in a restricted syntax language with defined semantics\<close>
|
||||
|
||||
Definition* [spcfy_def::concept, tag= "''specify''"]
|
||||
Definition* [spcfy_def, tag= "''specify''"]
|
||||
\<open>provide specific details about an entity in a rigorous and precise manner\<close>
|
||||
|
||||
Definition* [strct_conf_def::concept, tag="''strict conformance''"]
|
||||
Definition* [strct_conf_def, tag="''strict conformance''"]
|
||||
\<open>hierarchical relationship between a PP and an ST where all the requirements in the
|
||||
PP also exist in the ST
|
||||
|
||||
|
@ -344,36 +347,36 @@ Definition* [strct_conf_def::concept, tag="''strict conformance''"]
|
|||
be used for stringent requirements that are to be adhered to in a single
|
||||
manner. \<close>
|
||||
|
||||
Definition* [st_eval_def::concept, tag="''ST evaluation''"]
|
||||
Definition* [st_eval_def, tag="''ST evaluation''"]
|
||||
\<open>assessment of an ST against defined criteria\<close>
|
||||
|
||||
Definition* [subj_def::concept, tag="''subject''"]
|
||||
Definition* [subj_def, tag="''subject''"]
|
||||
\<open>active entity in the TOE that performs operations on objects\<close>
|
||||
|
||||
Definition* [toe::concept, tag= "''target of evaluation''"]
|
||||
Definition* [toe, tag= "''target of evaluation''"]
|
||||
\<open>set of software, firmware and/or hardware possibly accompanied by guidance\<close>
|
||||
|
||||
Definition* [thrt_agnt_def::concept, tag="''threat agent''"]
|
||||
Definition* [thrt_agnt_def, tag="''threat agent''"]
|
||||
\<open>entity that can adversely act on assets\<close>
|
||||
|
||||
Definition* [toe_eval_def::concept, tag="''TOE evaluation''"]
|
||||
Definition* [toe_eval_def, tag="''TOE evaluation''"]
|
||||
\<open>assessment of a TOE against defined criteria\<close>
|
||||
|
||||
Definition* [toe_res_def::concept, tag="''TOE resource''"]
|
||||
Definition* [toe_res_def, tag="''TOE resource''"]
|
||||
\<open>anything useable or consumable in the TOE\<close>
|
||||
|
||||
Definition* [toe_sf_def::concept, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"]
|
||||
Definition* [toe_sf_def, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"]
|
||||
\<open>combined functionality of all hardware, software, and firmware of a TOE that must be relied upon
|
||||
for the correct enforcement of the @{docitem sfr_def}s\<close>
|
||||
|
||||
Definition* [tr_vrb_def::concept, tag="''trace, verb''"]
|
||||
Definition* [tr_vrb_def, tag="''trace, verb''"]
|
||||
\<open>perform an informal correspondence analysis between two entities with only a
|
||||
minimal level of rigour\<close>
|
||||
|
||||
Definition* [trnsfs_out_toe_def::concept, tag="''transfers outside of the TOE''"]
|
||||
Definition* [trnsfs_out_toe_def, tag="''transfers outside of the TOE''"]
|
||||
\<open>TSF mediated communication of data to entities not under the control of the TSF\<close>
|
||||
|
||||
Definition* [transl_def::concept, tag= "''translation''"]
|
||||
Definition* [transl_def, tag= "''translation''"]
|
||||
\<open> describes the process of describing security requirements in a
|
||||
standardised language.
|
||||
|
||||
|
@ -381,45 +384,45 @@ use of the term translation in this context is not literal and does not imply
|
|||
that every SFR expressed in standardised language can also be translated
|
||||
back to the security objectives.\<close>
|
||||
|
||||
Definition* [trst_chan_def::concept, tag="''trusted channel''"]
|
||||
Definition* [trst_chan_def, tag="''trusted channel''"]
|
||||
\<open>a means by which a TSF and another trusted IT product
|
||||
can communicate with necessary confidence\<close>
|
||||
|
||||
Definition* [trst_it_prod_def::concept, tag="''trusted IT product''"]
|
||||
Definition* [trst_it_prod_def, tag="''trusted IT product''"]
|
||||
\<open>IT product, other than the TOE, which has its security functional requirements administratively coordinated with the TOE
|
||||
and which is assumed to enforce its security functional requirements correctly
|
||||
An example of a trusted IT product would be one that has been separately
|
||||
evaluated.\<close>
|
||||
|
||||
Definition* [trst_path_def::concept, tag="''trusted path''"]
|
||||
Definition* [trst_path_def, tag="''trusted path''"]
|
||||
\<open>means by which a user and a TSF can communicate with the necessary confidence\<close>
|
||||
|
||||
Definition* [tsf_data_def::concept, tag="''TSF data''"]
|
||||
Definition* [tsf_data_def, tag="''TSF data''"]
|
||||
\<open>data for the operation of the TOE upon which the enforcement of the SFR relies\<close>
|
||||
|
||||
Definition* [tsf_intrfc_def::concept, tag="''TSF interface''"]
|
||||
Definition* [tsf_intrfc_def, tag="''TSF interface''"]
|
||||
\<open>means by which external entities (or subjects in the TOE but outside of the TSF)
|
||||
supply data to the TSF, receive data from the TSF and invoke services from the TSF\<close>
|
||||
|
||||
Definition* [usr_def::concept, tag="''user''"] \<open>see external entity\<close>
|
||||
Definition* [usr_def, tag="''user''"] \<open>see external entity\<close>
|
||||
|
||||
Definition* [usr_datat_def::concept, tag="''user data''"]
|
||||
Definition* [usr_datat_def, tag="''user data''"]
|
||||
\<open>data for the user, that does not affect the operation of the TSF\<close>
|
||||
|
||||
Definition* [vrfy_def::concept, tag="''verify''"]
|
||||
Definition* [vrfy_def, tag="''verify''"]
|
||||
\<open>rigorously review in detail with an independent determination of
|
||||
sufficiency
|
||||
Also see “confirm”. This term has more rigorous connotations. The term
|
||||
“verify” is used in the context of evaluator actions where an independent
|
||||
effort is required of the evaluator.\<close>
|
||||
|
||||
Definition* [dev_def::concept, tag="''Developer''"]
|
||||
Definition* [dev_def, tag="''Developer''"]
|
||||
\<open>who respond to actual or perceived consumer security requirements in
|
||||
constructing a @{docitem toe_def}, reference this CC_Part_3
|
||||
when interpreting statements of assurance requirements and determining
|
||||
assurance approaches of @{docitem toe}s.\<close>
|
||||
|
||||
Definition*[evalu_def::concept, tag="'' Evaluator''"]
|
||||
Definition*[evalu_def, tag="'' Evaluator''"]
|
||||
\<open>who use the assurance requirements defined in CC_Part_3
|
||||
as mandatory statement of evaluation criteria when determining the assurance
|
||||
of @{docitem toe_def}s and when evaluating @{docitem pp_def}s and @{docitem st_def}s.\<close>
|
||||
|
|
|
@ -28,8 +28,20 @@ theory CENELEC_50128
|
|||
imports "../technical_report/technical_report"
|
||||
begin
|
||||
|
||||
(* this is a hack and should go into an own ontology, providing thingsd like:
|
||||
- Assumption*
|
||||
- Hypothesis*
|
||||
- Definition*. (Une redefinition de ce qui se passe dans tech-report, cible a semi-formal
|
||||
“Definitions of terminology” \<dots> )
|
||||
- Objective"
|
||||
- Claim*
|
||||
- Requirement*
|
||||
|
||||
*)
|
||||
|
||||
|
||||
text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for
|
||||
semi-formal terminology, which we re-use by this definition.\<close>
|
||||
semi-formal "math-alike" terminology, which we re-use by this definition.\<close>
|
||||
|
||||
doc_class semi_formal_content = math_content +
|
||||
status :: status <= "semiformal"
|
||||
|
@ -39,27 +51,29 @@ type_synonym sfc = semi_formal_content
|
|||
|
||||
(*>>*)
|
||||
|
||||
declare[[ Definition_default_class="semi_formal_content"]]
|
||||
|
||||
|
||||
text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
|
||||
|
||||
|
||||
section\<open>Terms and Definitions\<close>
|
||||
|
||||
typ "sfc"
|
||||
Definition*[assessment::sfc,short_name="''assessment''"]
|
||||
Definition*[assessment,short_name="''assessment''"]
|
||||
\<open>process of analysis to determine whether software, which may include
|
||||
process, documentation, system, subsystem hardware and/or software components, meets the specified
|
||||
requirements and to form a judgement as to whether the software is fit for its intended purpose.
|
||||
Safety assessment is focused on but not limited to the safety properties of a system.\<close>
|
||||
|
||||
Definition*[assessor::sfc, short_name="''assessor''"]
|
||||
Definition*[assessor, short_name="''assessor''"]
|
||||
\<open>entity that carries out an assessment\<close>
|
||||
|
||||
Definition*[COTS::sfc, short_name="''commercial off-the-shelf software''"]
|
||||
Definition*[COTS, short_name="''commercial off-the-shelf software''"]
|
||||
\<open>software defined by market-driven need, commercially available and whose fitness for purpose
|
||||
has been demonstrated by a broad spectrum of commercial users\<close>
|
||||
|
||||
|
||||
Definition*[component::sfc]
|
||||
Definition*[component]
|
||||
\<open>a constituent part of software which has well-defined interfaces and behaviour
|
||||
with respect to the software architecture and design and fulfils the following
|
||||
criteria:
|
||||
|
@ -71,53 +85,53 @@ criteria:
|
|||
\<close>
|
||||
typ "sfc"
|
||||
|
||||
Definition*[CMGR::sfc, short_name="''configuration manager''"]
|
||||
Definition*[CMGR, short_name="''configuration manager''"]
|
||||
\<open>entity that is responsible for implementing and carrying out the processes
|
||||
for the configuration management of documents, software and related tools including
|
||||
\<^emph>\<open>change management\<close>\<close>
|
||||
|
||||
Definition*[customer::sfc]
|
||||
Definition*[customer]
|
||||
\<open>entity which purchases a railway control and protection system including the software\<close>
|
||||
|
||||
Definition*[designer::sfc]
|
||||
Definition*[designer]
|
||||
\<open>entity that analyses and transforms specified requirements into acceptable design solutions
|
||||
which have the required safety integrity level\<close>
|
||||
|
||||
Definition*[entity::sfc]
|
||||
Definition*[entity]
|
||||
\<open>person, group or organisation who fulfils a role as defined in this European Standard\<close>
|
||||
|
||||
declare_reference*[fault::sfc]
|
||||
Definition*[error::sfc]
|
||||
declare_reference*[fault]
|
||||
Definition*[error]
|
||||
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour (cf. @{semi_formal_content (unchecked) \<open>fault\<close>}))\<close>
|
||||
|
||||
Definition*[fault::sfc]
|
||||
Definition*[fault]
|
||||
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour (cf @{semi_formal_content \<open>error\<close>})\<close>
|
||||
|
||||
Definition*[failure::sfc]
|
||||
Definition*[failure]
|
||||
\<open>unacceptable difference between required and observed performance\<close>
|
||||
|
||||
Definition*[FT::sfc, short_name="''fault tolerance''"]
|
||||
Definition*[FT, short_name="''fault tolerance''"]
|
||||
\<open>built-in capability of a system to provide continued correct provision of service as specified,
|
||||
in the presence of a limited number of hardware or software faults\<close>
|
||||
|
||||
Definition*[firmware::sfc]
|
||||
Definition*[firmware]
|
||||
\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a
|
||||
way that is functionally independent of applicative software\<close>
|
||||
|
||||
Definition*[GS::sfc,short_name="''generic software''"]
|
||||
Definition*[GS,short_name="''generic software''"]
|
||||
\<open>software which can be used for a variety of installations purely by the provision of
|
||||
application-specific data and/or algorithms\<close>
|
||||
|
||||
Definition*[implementer::sfc]
|
||||
Definition*[implementer]
|
||||
\<open>entity that transforms specified designs into their physical realisation\<close>
|
||||
|
||||
Definition*[integration::sfc]
|
||||
Definition*[integration]
|
||||
\<open>process of assembling software and/or hardware items, according to the architectural and
|
||||
design specification, and testing the integrated unit\<close>
|
||||
|
||||
Definition*[integrator::sfc]
|
||||
Definition*[integrator]
|
||||
\<open>entity that carries out software integration\<close>
|
||||
|
||||
Definition*[PES :: sfc, short_name="''pre-existing software''"]
|
||||
|
@ -127,52 +141,52 @@ off-the shelf) and open source software\<close>
|
|||
Definition*[OSS :: sfc, short_name="''open source software''"]
|
||||
\<open>source code available to the general public with relaxed or non-existent copyright restrictions\<close>
|
||||
|
||||
Definition*[PLC::sfc, short_name="''programmable logic controller''"]
|
||||
Definition*[PLC, short_name="''programmable logic controller''"]
|
||||
\<open>solid-state control system which has a user programmable memory for storage of instructions to
|
||||
implement specific functions\<close>
|
||||
|
||||
Definition*[PM::sfc, short_name="''project management''"]
|
||||
Definition*[PM, short_name="''project management''"]
|
||||
\<open>administrative and/or technical conduct of a project, including safety aspects\<close>
|
||||
|
||||
Definition*[PGMGR::sfc, short_name="''project manager''"]
|
||||
Definition*[PGMGR, short_name="''project manager''"]
|
||||
\<open>entity that carries out project management\<close>
|
||||
|
||||
Definition*[reliability::sfc]
|
||||
Definition*[reliability]
|
||||
\<open>ability of an item to perform a required function under given conditions for a given period of time\<close>
|
||||
|
||||
Definition*[robustness::sfc]
|
||||
Definition*[robustness]
|
||||
\<open>ability of an item to detect and handle abnormal situations\<close>
|
||||
|
||||
Definition*[RMGR::sfc, short_name="''requirements manager''"]
|
||||
Definition*[RMGR, short_name="''requirements manager''"]
|
||||
\<open>entity that carries out requirements management\<close>
|
||||
|
||||
Definition*[RMGMT::sfc, short_name="''requirements management''"]
|
||||
Definition*[RMGMT, short_name="''requirements management''"]
|
||||
\<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and
|
||||
then controlling change and communicating to relevant stakeholders. It is a continuous process
|
||||
throughout a project\<close>
|
||||
|
||||
Definition*[risk::sfc]
|
||||
Definition*[risk]
|
||||
\<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by
|
||||
a hazard) and the degree of severity of that harm\<close>
|
||||
|
||||
Definition*[safety::sfc]
|
||||
Definition*[safety]
|
||||
\<open>freedom from unacceptable levels of risk of harm to people\<close>
|
||||
|
||||
Definition*[SA::sfc, short_name="''safety authority''"]
|
||||
Definition*[SA, short_name="''safety authority''"]
|
||||
\<open>body responsible for certifying that safety related software or services comply with relevant
|
||||
statutory safety requirements\<close>
|
||||
|
||||
Definition*[SF::sfc, short_name="''safety function''"]
|
||||
Definition*[SF, short_name="''safety function''"]
|
||||
\<open>a function that implements a part or whole of a safety requirement\<close>
|
||||
|
||||
Definition*[SFRS::sfc, short_name= "''safety-related software''"]
|
||||
Definition*[SFRS, short_name= "''safety-related software''"]
|
||||
\<open>software which performs safety functions\<close>
|
||||
|
||||
Definition*[software::sfc]
|
||||
Definition*[software]
|
||||
\<open>intellectual creation comprising the programs, procedures, rules, data and any associated
|
||||
documentation pertaining to the operation of a system\<close>
|
||||
|
||||
Definition*[SB::sfc, short_name="''software baseline''"]
|
||||
Definition*[SB, short_name="''software baseline''"]
|
||||
\<open>complete and consistent set of source code, executable files, configuration files,
|
||||
installation scripts and documentation that are needed for a software release. Information about
|
||||
compilers, operating systems, preexisting software and dependent tools is stored as part of the
|
||||
|
@ -183,7 +197,7 @@ released and assessed
|
|||
|
||||
|
||||
|
||||
Definition*[SWLC::sfc, short_name="''software life-cycle''"]
|
||||
Definition*[SWLC, short_name="''software life-cycle''"]
|
||||
\<open>those activities occurring during a period of time that starts when
|
||||
software is conceived and ends when the software is no longer available for use. The software life
|
||||
cycle typically includes a requirements phase, design phase,test phase, integration phase,
|
||||
|
@ -191,35 +205,35 @@ deployment phase and a maintenance phase 3.1.35 software maintainability
|
|||
capability of the software to be modified; to correct faults, improve to a different environment
|
||||
\<close>
|
||||
|
||||
Definition*[SM::sfc, short_name="''software maintenance''"]
|
||||
Definition*[SM, short_name="''software maintenance''"]
|
||||
\<open> action, or set of actions, carried out on software after deployment functionality
|
||||
performance or other attributes, or adapt it with the aim of enhancing or correcting its\<close>
|
||||
|
||||
Definition*[SOSIL::sfc, short_name="''software safety integrity level''"]
|
||||
Definition*[SOSIL, short_name="''software safety integrity level''"]
|
||||
\<open>classification number which determines the techniques and measures that have to be applied to
|
||||
software NOTE Safety-related software has been classified into five safety integrity levels, where
|
||||
0 is the lowest and 4 the highest.\<close>
|
||||
|
||||
Definition*[supplier::sfc]
|
||||
Definition*[supplier]
|
||||
\<open>entity that designs and builds a railway control and protection system including the software
|
||||
or parts thereof\<close>
|
||||
|
||||
Definition*[SYSIL::sfc, short_name="''system safety integrity level''"]
|
||||
Definition*[SYSIL, short_name="''system safety integrity level''"]
|
||||
\<open>classification number which indicates the required degree of confidence that an integrated
|
||||
system comprising hardware and software will meet its specified safety requirements\<close>
|
||||
|
||||
Definition*[tester::sfc]\<open>an entity that carries out testing\<close>
|
||||
Definition*[tester]\<open>an entity that carries out testing\<close>
|
||||
|
||||
Definition*[testing::sfc]
|
||||
Definition*[testing]
|
||||
\<open>process of executing software under controlled conditions as to ascertain its behaviour and
|
||||
performance compared to the corresponding requirements specification\<close>
|
||||
|
||||
Definition*[TCT1::sfc, short_name="''tool class T1''"]
|
||||
Definition*[TCT1, short_name="''tool class T1''"]
|
||||
\<open>generates no outputs which can directly or indirectly contribute to the executable code
|
||||
(including data) of the software NOTE 11 examples include: a text editor or a requirement or
|
||||
design support tool with no automatic code generation capabilities; configuration control tools.\<close>
|
||||
|
||||
Definition*[TCT2::sfc,short_name="''tool class T2''"]
|
||||
Definition*[TCT2,short_name="''tool class T2''"]
|
||||
\<open>supports the test or verification of the design or executable code, where errors in the tool
|
||||
can fail to reveal defects but cannot directly create errors in the executable software
|
||||
NOTE T2 examples include: a test harness generator; a test coverage measurement tool; a static
|
||||
|
@ -227,35 +241,35 @@ analysis tool. reproduce defined versions and be the input for future releases a
|
|||
at upgrade in the maintenance phase
|
||||
\<close>
|
||||
|
||||
Definition*[TCT3::sfc, short_name="''tool class T3''"]
|
||||
Definition*[TCT3, short_name="''tool class T3''"]
|
||||
\<open>generates outputs which can directly or indirectly contribute to the executable code
|
||||
(including data) of the safety related system NOTE T3 examples include: a source code compiler,
|
||||
a data/algorithms compiler, a tool to change set-points during system operation; an optimising
|
||||
compiler where the relationship between the source code program and the generated object code is
|
||||
not obvious; a compiler that incorporates an executable run-time package into the executable code.
|
||||
\<close>
|
||||
Definition*[traceability::sfc, short_name="''traceability''"]
|
||||
Definition*[traceability, short_name="''traceability''"]
|
||||
\<open>degree to which relationship can be established between two or more products of a development
|
||||
process, especially those having a predecessor/successor or master/subordinate relationship to one
|
||||
another\<close>
|
||||
|
||||
Definition*[validation::sfc, short_name="''validation''"]
|
||||
Definition*[validation, short_name="''validation''"]
|
||||
\<open>process of analysis followed by a judgment based on evidence to
|
||||
documentation, software or application) fits the user needs,in particular with respect to safety
|
||||
and quality and determine whether an item (e.g. process, with emphasis on the suitability of its
|
||||
operation in accordance to its purpose in its intended environment\<close>
|
||||
|
||||
Definition*[validator::sfc, short_name="''validator''"]
|
||||
Definition*[validator, short_name="''validator''"]
|
||||
\<open>entity that is responsible for the validation\<close>
|
||||
|
||||
Definition*[verification::sfc, short_name="''verification''"]
|
||||
Definition*[verification, short_name="''verification''"]
|
||||
\<open>process of examination followed by a judgment based on evidence that output items (process,
|
||||
documentation, software or application) of a specific development phase fulfils the requirements of
|
||||
that phase with respect to completeness, correctness and consistency.
|
||||
NOTE Verification is mostly based on document reviews (design, implementation, test documents etc.).
|
||||
\<close>
|
||||
|
||||
Definition*[verifier::sfc, short_name="''verifier''"]
|
||||
Definition*[verifier, short_name="''verifier''"]
|
||||
\<open>entity that is responsible for one or more verification activities\<close>
|
||||
|
||||
|
||||
|
|
|
@ -189,8 +189,21 @@ doc_class math_content = tc +
|
|||
invariant s2 :: "\<lambda> \<sigma>::math_content. status \<sigma> = semiformal"
|
||||
type_synonym math_tc = math_content
|
||||
|
||||
text\<open>The class \<^typ>\<open>math_content\<close> is perhaps more adequaltely described as "math-alike content".
|
||||
Sub-classes can englobe instances such as:
|
||||
\<^item> terminological definitions such as:
|
||||
\<open>Definition*[assessor::sfc, short_name="''assessor''"]\<open>entity that carries out an assessment\<close>\<close>
|
||||
\<^item> free-form mathematical definitions such as:
|
||||
\<open>Definition*[process_ordering, short_name="''process ordering''"]\<open>
|
||||
We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>, where \<^vs>\<open>-0.2cm\<close>
|
||||
1) \<^vs>\<open>-0.2cm\<close> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
|
||||
2) ...
|
||||
\<close>\<close>
|
||||
\<^item> semi-formal descriptions, which are free-form mathematical definitions on which finally
|
||||
an attribute with a formal Isabelle definition is attached.
|
||||
|
||||
\<close>
|
||||
|
||||
find_theorems name:"s1" name:"scholarly"
|
||||
|
||||
(* type qualification is a work around *)
|
||||
|
||||
|
|
Loading…
Reference in New Issue