This file is in construction. Its concepts specialize the
top-level information security related concepts represented in this other file.
The representations are written in the FL notation.
1. Short typology of security related concepts
2. Formalization of security attributes and requirements
3. Other representation stuff
4. Other projects
5. Modelisation examples of the 6/09/2012
thing > thing_playing_some_role {( entity situation )} ;
security_related_thing < thing_playing_some_role, //warning: may lead to not see some pbs
> {( security_related_entity security_related_situation )}
(security_related_agent //= thing_agent_of_a_security_supporting/threatening_process
> (security_supporting_thing > threat vulnerability risk)
(security_threatening_thing > fail-safe_thing)
)
(security_related_object //= thing_object_of_a_security_supporting/threatening_process
//thing__object__of__a__support--that--has--for--object--a--process
> thing_object_of_security_supporting_process
thing_that_is_at_low_risk_of_beling_object_of_security_threatening_process
thing_that_is_at_high_risk_of_beling_object_of_security_threatening_process
)
{ invulnerable_thing vulnerable_thing }; //avoid using! Instead, represent things as
// object of one or several kinds of security_threatening_process (see below)
security_related_entity < entity,
> { (security_related_attribute < attribute_or_quality_or_measure,
> (assurance_level___degree_of_security_strength < security_supporting_thing)
(security_attribute
> #accessibility #integrity #dependability {#dangerousness #safeness}
dependancy_or_information_security_attribute #confidentiality.discreetness
) //avoid using! Instead, represent things as object of one or several
// subkinds of security_supporting_process (see below)
)
(security_related_description < pm#description, //description_content/medium
> security_supporting_regulation security_policy security_model
security_principle security_measure_description
description_of_safe_architecture
security_related_certification
security_evaluation_result_description security_supporting_skill_qualification
(security_protocol < #protocol) //pm: to check
(security_supporting_language
> computer_security_policy_language security_supporting_programming_language)
(security_supporting_program
> firewall )
)
(security_related_physical_object < physical_object,
> (security_supporting_physical_object < security_supporting_thing)
(security_threatening_physical_object < security_threatening_thing)
)
(security_related_agent_entity < pm#causal_entity,
> {security_related_organisation security_related_individual}
(security_supporting_agent_entity < security_supporting_thing )
(security_threatening_agent_entity < security_threatening_thing)
//avoid using! Instead, represent such things as agent of one or several kinds
// of security_supporting_process or security_threatening_process (see below)
)
};
security_related_situation < situation,
> {( (security_related_state < state,
> {#safety.state #danger.state} #insecurity.feeling
)
(security_related_process < process,
> (process_object_of_a_security_supporting/threatening_process //avoid using!
> (process_typically_object_of_a_security_supporting/threatening_process
> communication)
)
(security_threatening_process < security_threatening_thing,
> process_threatening_the_security_of_a_communication //avoid using?
// := `a process agent of a threatening with object a communication'
)
(security_supporting_process < security_supporting_thing,
> risk_management_process security_evaluation
(applying_one_or_several_security_by_design_principles
> applying_the_principle_of_least_privilege
applying_the_defense_in_depth_principle
applying_the_fail_secure_principle
)
(supporting_access_control
> {discretionary_access_control mandatory_access_control
role-based_access_control}
{role-based_access_control user-based_access_control}
)
(trusted_process
:=> "roots of trust for the process should not be changed"
> trusted_authentication trusted_integrity_support
)
(supporting_at_least_one_particular_security_attribute
> supporting_confidentiality supporting_integrity
supporting_availability supporting_interoperability
supporting_imputability
(supporting_authenticity
> (authentication
> (trusted_authentication < trusted_process) )
)
)
)
)};
integrity_of_a_quantum_of_information_between_two_given_dates
attribute of: (a quantum_of_information ?qi1, object of: (a storage, place: a place ?place, time: ?t1)),
< state, //???
:= [?qi1 = (?qi2, object of: (a storage, place: ?place, time: (?t2 > ?t1))] //2.1.1.2, p4
< (non-modification < boolean),
object of: checking_the_integrity_of_a_quantum_of_information_between_two_given_dates
(supporting_the_integrity_of_a_quantum_of_information_between_two_given_dates
definition: "task aimed to prevent the unauthorized/accidental
modification/deletion of a certain quantum of
information stored in a certain repository";
authenticated_process (?p)
//:= (a process attribute: authenticity_of_a_process),
:= (a process object of: an ?authenticating_action);
evita_flashing < authenticated_process,
attribute: authenticity_of_a_process,
object of: an ?authenticating_action;
authenticity < state,
> authenticity_of_the_origin_of_data
(authenticity_of_a_process (?p)
:= [?p object of: an ?authenticating_action] //2.1.2.3.1, p 9
> (evita#Authenticity_1
:= (every (active_braking, agent: (a car driver: a person),
trigger: some enviroment_information ?ei),
must have for precondition:
[?ei type: origin_authentic content_authentic time_authentic]
))
/* (evita#Authenticity_102
:= (every (gateway recipient of:
(a flashing_command,
object of: (a sending from: an ECU ?e1, to: an ECU ?e2,
via: ?g),
must have for precondition:
[?ff object of: an access_control] //Evita 3.2.4, p35r45
))
*/ (evita#Authenticity_102
:= (every (ECU recipient of: (a flashing_command part: a code ?c))
must be agent of: (a authentication
object: (the organisation author of: ?c),
attribute:
)
)),
// := every ECU type: evita#authenticated_artefact_102 //oui
// := every ECU attribute: evita#Authenticity_attribute_102; //non
);
evita#authenticated_artefact_102 (?a) < artefact,
:= (an artefact ?a
recipient of: (a evita#authenticated_process_101l //e.g., flashing_command
part: a code ?c))
must be agent of: (a authentication
object: (the organisation author of: ?c),
attribute:
)
)
evita#authenticated_process_101 (?a) < process, //flashing_command as action
:= (a process
evita#authenticated_description_101 (?d) < description, //as message
:=
//if expert writes a rule, the rule must be true and as general and precise as possible
//=> expert must correct/add in higher rules (even those of libraries) what he discovers in
// lower rules ; example for article : information on trust -> top-level rules
// autre exemple: flashing_command used for another embedded system : insert "niveau" before EVITA
//?x "marked as sensitive" <= ?x may be object of: (an attack result: disaster according to ?sensitiveMarker)
any relation from a process ?w,
that is marked as sensitive by "someone authorised to do so" ?sensitiveMarker,
must be checked by 'a checker ?ca trusted by ?sensitiveMarker'
at least for a property ?prop on '?w or related to ?w'
> (any writing ?w of a description ?d by an agent ?a with initiator ?requester,
into a location ?l marked as sensitive by "someone authorised to do so" ?sensitiveMarker,
must be checked by 'a checker ?ca trusted by ?sensitiveMarker'
at least for a property ?prop on '?w or related to ?w' //?d, ?a, ?l, ...
> buffer overflow protection rule here,
> (any writing ?w of ?d by ... into ?l marked as ...
must be checked by ?ca BEFORE ?w
at least for a property ?prop on '?w or related to ?w'
so that ?w authorised by ?a //???
> (any writing ?w of a MESSAGE (?d part: a code,
part: (?authorshipOfCode proof of: [?d author: ?x])
//YR: verifier si preuve d'integrite egalement ?
by an agent ?a with initiator ?requester
into a MICRO-CONTROLER ?l=?a marked as ...
must be checked by ?ca BEFORE ?w
at least for property ?prop ON ?x //e.g. ?x est en liste blanche
so that ?w authorised by ?a //???
> any FLASHING_COMMAND ?w of a MESSAGE (?d part: a code,
part: (?authorshipOfCode proof of: [?d author: ?x])
by an ECU ?a with initiator ?requester
into an ECU ?l=?a marked as sensitive by CARMAKER ?sensitiveMarker
must be checked by an ECU ?a WITH INITIATOR ?requester before ?w
at least for property ?prop ON ?x //e.g. ?x est en liste blanche
so that ?w authorised by ?a //???
)
)
)
writing < process;
flashing_command < writing of code ;
ECU < micro-controler, part of: a car ;
CARMAKER authorised to do attribute trust to any part of a car ;
//our method/software should be able to detect contradictions between security rules,
// e.g., chiffrement vs. signature
access_control
definition: "controlling and selectively authorizing access of subjects to objects",
subtask: 1..* supporting_authentication,
> {discretionary_access_control mandatory_access_control role-based_access_control}
{role-based_access_control user-based_access_control}
(evita#Access_101
:= (every sending ?s, //=============== 1st version
every (ECU , recipient of: (?s agent: an agent ?sender,
object: a flashing_command ?fc),
part: (a code, for: ?fc)
)
must be agent of: (an access_control object:
[?sender may be agent of: (a sending, object: ?fc)]
));
:= (every (sending ?s, //=============== 2nd version
agent: an agent ?sender,
object: a flashing_command ?fc,
recipient: (an ECU ?ecu, part: (a code, for: ?fc))
)
precondition:
(?ecu trusted_by: ?ecu,
agent of: (an access_control object:
[?sender may be agent of: ?s]
))
)
);
(every (sending ?s //======== Some more general stuff ========= 3.2.4, p 35
agent: an agent ?sender,
object: a flashing_command ?fc,
recipient: (an ECU ?ecu, part: (a code, for: ?fc))
)
precondition:
[an agent ?a
trusted_by: ?ecu,
agent of: (an access_control
object: [?sender may be agent of: ?s]
result: (?message_s_isAllowed
object of: (a comm, agent: ?a, to: ?ecu),
object of: (a verif_I+O, agent: ?ecu)
)
))
]);
//==================== More generic versions ======================================
I+O_verified_sending_where_recipient_does_the_verification (?s)
:= (a sending ?s agent: an agent ?sender, object: a message ?message,
recipient: an agent ?recipient,
postcondition:
[?recipient agent of: (a I+O_verification
object: [?message from: ?sender]
object: [?message not_modified...]
)]);
verified_sending ( ?vs)
:= (a sending ?vs agent: an agent ?sender, message: a message ?message,
recipient: an agent ?recipient,
attribute: ?prop,
(post-)condition:
OR{ [?recipient prop: ?x ?y ?z,
agent of: (a verification parameter: ?prop,
object: [?message from: ?sender]
object: [?message not_modified...]
)]
[an agent ?a != ?recipient,
trusted_by: ?recipient, prop: ?x ?y ?z,
agent of: (a verification parameter: ?prop,
object: [?message from: ?sender]
object: [?message not_modified...]
result: (?message_s_isVerified
message of: (a verified_sending
parameter: (prop2
result of:
(propGen param: ?x))
)
))
});
[every flashing_command
must be object of: (a verified_sending param: propGen_I_techX_then_O)];
ECU_223 prop: x_412 y_66;
propGen
> propGen_I_techX_then_O propGen_O_tech_Y;
propGen_I_techX_then_O
:= (a propGen param: ...,
result: ...
);
//note: to allow copy-pasting, Yves should send Ph. the doc. sources
//======== typology of attack goal and attack tree
attack
goal: (. attack_goal
> (harming
> harming_an_individual ....
)
)_[any->a; a<-any]
any thing_that_is_at_high_risk_of_being_object_of_security_threatening_process
has been object of: (a security_evaluation, result: "high risk"),
should be object of: (a trusted_authentication
subprocess: ...
tool: ...
),
should be object of: (a trusted_integrity_support
subprocess: ...
tool: ...
);
//org. plus simple (-redondante)? cf. apd. p. 64..., 69... attack tree
//======== other :
2.5) pb. organisation semantique // p. 125 :
process_to_ensure_the_security_requirements_of_Evita
> (gsr-1
name: preventing_malicious_modifications_on_the_environment_representation,
descr: "preventing_attackers_from_feeding_wrong_information_to_gateways" //spec?
> (gsr-1.3
name: authenticating_messages_sources
descr: "authenticating_changes_sent_from_other_cars and authenticating_sensors"
> (gsr-1.3.1 < trusted_authentication,
name: enforce_trusted_authentication
)
)
);
authenticating__message-sources :=
< authentication_of_a_message_source
object: (?s source of: a message)
I) security for my knowledge-base cooperation approach
II) Adapt our results about cars to source code ? ...
yes, especially II.1 since high-level ... methodology
process
> (security_supporting_process/technique
> (security_supporting_process_against_a_certain_attack_model
counterbalance of: some security_defeating_process_for_a_certain_kind_of_attacker
)
(protocol)
part: ...
)
(password_encoding input: a password, output: an encoded_password,
> (password_encoding_without_salting support: an OS,
output: (an encoded_password object of: a precomputed_enumeration_attack)
)
(authentication_encoding_with_salting parameter: a salt_data,
input: an encoded_password, output: an acceptation_or_not
)
)
(password_encoding input: a password, output: an encoded_password)
)
(security_defeating_process/technique
> (enumeration_attack object: an encoded_password ?ep,
> (precomputed_enumeration_attack
duration_ratio: attack_pwd_hash_lookup_table_duration_computation
(length(?ep),
length(?salt parameter of: (a password_encoding_with_salting ?pes
output: ?ep),
hash_length_used_by_this_os(?os support of: ?pes)
)),
// > precomputed_enumeration_attack_taking_6_months
)
)
(security_defeating_process_for_a_certain_kind_of_attacker //attack model
> (security_defeating_process_by_amateur_hacker
support: (a disc volume: (a volume less than: 1000 Gb)
> ...
)
)
),
instance: (my_overall_process_that_run_my_system
security_support: some security_supporting_process_against_a_certain_attack_model,
support: (a system duration: 10 years,
part: (a disc length: 500Mb), software: an OS,
part: (a sending_data_to_micro_controler_by_server
max_retry: 10,
duration: (a duration less than: 10s),
part: (... part: (a password_encoding
duration_ratio: (a value less than 6 mo?x)
))
)
);
//see if bugs can be automatically found by examining the graph of the code or its test results
(def_function attack_pwd_hash_lookup_table_duration_computation
(?pwd_length ?salt_length ?hash_length) :=
(* (pwd_hash_lookup_table_duration_ratio_computation ?pwd_length ?salt_length ?hash_length)
(+ (duration_of_encoding_of (authentication_encoding_with_salting ...)
))
(def_function attack_pwd_hash_lookup_table_duration_ratio_computation
(?pwd_length ?salt_length ?hash_length) :=
(/ (+ ?pwd_length ?salt_length) ?hash_length)
)
================ 11/01/2013
generation, par nous, de
1) code à nous
2) explications (+ code détection d'erreurs)
pour deboggage du code ou,
si intrusion, debogagge de règles|modèle|spec. de sécurité
3) code de 'debogage pour test cases sur code non généré par nous' ???
security (Design) Pattern //for J2EE chris steel
component-based softwre engineering + security + odel-driven
protection
> protection minimale necessaire //
principes|criteria|attri
> design patter
comp générique
comp / env
code généré
reference monitor
input: (modification pre post
output: ok