diff --git a/docs/requirements.rst b/docs/requirements.rst
index 3af74b14d89b6c8c6c75f97c681fb009b3e84d2c..3e03d6a378b1f6f23acbd367c413fba112a97f8f 100644
--- a/docs/requirements.rst
+++ b/docs/requirements.rst
@@ -73,6 +73,7 @@ ID: ``all_concrete_map_something``
Makes sure each concrete infrastructure element is mapped to a node in the Abstract Infrastructure Layer.
+
Network Interfaces belong to a Security Group
---------------------------------------------
@@ -83,11 +84,26 @@ ID: ``security_group_must_have_iface``
Makes sure all network interfaces have been configured to belong to a security group.
This way, the user will be reminded to configure adequate rules for each network.
-External Services are reached through HTTPS
--------------------------------------------
- All external SaaS can be reached only through a secure connection.
+Virtual Machines in AutoScaleGroup should not be present in Concretization
+--------------------------------------------------------------------------
+
+ID: ``concrete_asg_no_vm``
+
+*Available from DOML v2.2+*
+
+Makes sure a VM present inside an AutoScaleGroup in the Infrastructure Layer is not present
+and mapped in the Concretization layer.
+
+
+.. Deprecated
+
+.. External Services are reached through HTTPS
+.. -------------------------------------------
+
+.. All external SaaS can be reached only through a secure connection.
+
+.. ID: ``external_services_must_have_https``
-ID: ``external_services_must_have_https``
+.. Makes sure that an HTTPS rule is enforced for a Network Interface of a Software Component that interfaces with a SaaS.
-Makes sure that an HTTPS rule is enforced for a Network Interface of a Software Component that interfaces with a SaaS.
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/builtin_requirements/__init__.py b/mc_openapi/doml_mc/builtin_requirements/__init__.py
index e5d2d8dec45778cc6667e45b8eb4b23ba965bbeb..7406583a43c2cde003c77e1729bf5a6dcb5b4c7c 100644
--- a/mc_openapi/doml_mc/builtin_requirements/__init__.py
+++ b/mc_openapi/doml_mc/builtin_requirements/__init__.py
@@ -4,7 +4,7 @@ CELEMS_V2_0 = [
("infrastructure_Network", "concrete_RuntimeProvider::networks", "concrete_Network::maps"),
("infrastructure_Storage", "concrete_RuntimeProvider::storages", "concrete_Storage::maps"),
("infrastructure_FunctionAsAService", "concrete_RuntimeProvider::faas","concrete_FunctionAsAService::maps"),
- ("infrastructure_ComputingGroup", "concrete_RuntimeProvider::group","concrete_ComputingGroup::maps")
+ ("infrastructure_ComputingGroup", "concrete_RuntimeProvider::group","concrete_ComputingGroup::maps"),
]
from .vm_has_iface import VM_HAS_IFACE, VM_HAS_IFACE_V2_3
@@ -14,6 +14,7 @@ from .all_software_components_deployed import ALL_SOFTWARE_COMPONENTS_DEPLOYED
from .all_infrastructure_elements_deployed import ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED
from .all_concrete_maps_something import ALL_CONCRETE_MAP_SOMETHING
from .security_group_must_have_iface import SECURITY_GROUP_MUST_HAVE_IFACE
+from .concrete_asg_no_vm import CONCRETE_ASG_NO_VM
__ALL__ = [
VM_HAS_IFACE,
@@ -25,5 +26,6 @@ __ALL__ = [
ALL_SOFTWARE_COMPONENTS_DEPLOYED,
ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
ALL_CONCRETE_MAP_SOMETHING,
- SECURITY_GROUP_MUST_HAVE_IFACE
+ SECURITY_GROUP_MUST_HAVE_IFACE,
+ CONCRETE_ASG_NO_VM
]
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py b/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py
index 05a1bbd1556a174365a0c167c5e1c0abbd4996a4..0d0f366cf1b018a0f0534642a1e65568115254d1 100644
--- a/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py
+++ b/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py
@@ -45,8 +45,28 @@ def all_infrastructure_elements_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts
ielemClass, providerAssoc, celemAssoc
)
for ielemClass, providerAssoc, celemAssoc in CELEMS_V2_0
- if ielemClass != 'infrastructure_VirtualMachine' # handle special case separately below
+ if ielemClass != 'infrastructure_VirtualMachine' # handle special case separately in concrete_asg_no_vm and below
),
+ And(
+ smtenc.element_class_fun(ielem) == smtenc.classes["infrastructure_VirtualMachine"],
+ Not(Exists([asg],
+ Or(
+ smtenc.association_rel(
+ asg, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], ielem),
+ Exists(
+ [provider, celem],
+ And(
+ smtenc.association_rel(
+ concr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
+ smtenc.association_rel(
+ provider, smtenc.associations["concrete_RuntimeProvider::vms"], celem),
+ smtenc.association_rel(
+ celem, smtenc.associations["concrete_VirtualMachine::maps"], ielem)
+ )
+ )
+ )
+ ))
+ )
)
)
diff --git a/mc_openapi/doml_mc/builtin_requirements/concrete_asg_no_vm.py b/mc_openapi/doml_mc/builtin_requirements/concrete_asg_no_vm.py
new file mode 100644
index 0000000000000000000000000000000000000000..445e8e9d13c3fb98fc73bf54acf022f763f6c16e
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/concrete_asg_no_vm.py
@@ -0,0 +1,43 @@
+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+
+def concrete_asg_no_vm(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+ ielem, concr, provider, celem, asg = Consts("ielem concr provider celem asg", smtsorts.element_sort)
+ return And(
+ smtenc.element_class_fun(
+ concr) == smtenc.classes["concrete_ConcreteInfrastructure"],
+ # We don't want the following to happen:
+ # If exists ASG(infr) -> VM(infr), then exists a VM(concr) -> VM(infr)
+ And(
+ smtenc.element_class_fun(ielem) == smtenc.classes["infrastructure_VirtualMachine"],
+ smtenc.association_rel(
+ asg, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], ielem),
+ (Exists(
+ [celem],
+ smtenc.association_rel(celem, smtenc.associations["concrete_VirtualMachine::maps"], ielem)
+ ))
+ )
+ )
+
+
+def ed_concrete_asg_no_vm(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+ try:
+ ielem = Const("ielem", smtsorts.element_sort)
+ asg = Const("asg", smtsorts.element_sort)
+ ielem_name = get_user_friendly_name(
+ intermediate_model, solver.model(), ielem)
+ if ielem_name:
+ return f"Virtual machine '{ielem_name}' in AutoScale Group '{asg}' should not be present in the concretization layer."
+ except:
+ return "Any virtual machine in an AutoScale Group should not be present in the concretization layer."
+
+MSG = "All virtual machines in an autoscale group in the infrastructure layer should not be mapped in the concretization layer."
+
+CONCRETE_ASG_NO_VM = (
+ concrete_asg_no_vm,
+ "concrete_asg_no_vm",
+ MSG,
+ ed_concrete_asg_no_vm
+)
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/common_reqs.py b/mc_openapi/doml_mc/common_reqs.py
index bab95408a9da6b5e3352b139511623e0f6102df1..f49cf80987cc84aae87221d453a253b41b6fea82 100644
--- a/mc_openapi/doml_mc/common_reqs.py
+++ b/mc_openapi/doml_mc/common_reqs.py
@@ -29,7 +29,8 @@ REQUIREMENTS = {
ALL_SOFTWARE_COMPONENTS_DEPLOYED,
ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
ALL_CONCRETE_MAP_SOMETHING,
- SECURITY_GROUP_MUST_HAVE_IFACE
+ SECURITY_GROUP_MUST_HAVE_IFACE,
+ CONCRETE_ASG_NO_VM
],
DOMLVersion.V2_3: [
VM_HAS_IFACE_V2_3,
@@ -38,7 +39,8 @@ REQUIREMENTS = {
ALL_SOFTWARE_COMPONENTS_DEPLOYED,
ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
ALL_CONCRETE_MAP_SOMETHING,
- SECURITY_GROUP_MUST_HAVE_IFACE
+ SECURITY_GROUP_MUST_HAVE_IFACE,
+ CONCRETE_ASG_NO_VM
],
}
diff --git a/tests/test_modelchecker.py b/tests/test_modelchecker.py
index ac9355f16b6261be9d1a55c7dfd0ff61a6075635..a4d60c9e18668700a95848e039f280afd2919712 100644
--- a/tests/test_modelchecker.py
+++ b/tests/test_modelchecker.py
@@ -56,13 +56,13 @@ OUTPUT = {
'v2.2': {
'faas.domlx': 'unsat',
'iot_simple_app.domlx': 'unsat',
- 'nginx-aws-ec2.domlx': 'sat',
+ 'nginx-aws-ec2.domlx': 'unsat', # was sat before concrete_asg_no_vm req
'nginx_func_req2_unsat.domlx': 'unsat',
'nginx_func_req2_unsat_neg.domlx': 'unsat',
- 'nginx_func_req_neg.domlx': 'sat',
- 'nginx-csp-compatibility-test.domlx': 'sat',
- 'nginx_func_req.domlx': 'sat',
- 'nginx_flags.domlx': 'sat'
+ 'nginx_func_req_neg.domlx': 'unsat', # ditto
+ 'nginx-csp-compatibility-test.domlx': 'unsat', # ditto
+ 'nginx_func_req.domlx': 'unsat', # ditto
+ 'nginx_flags.domlx': 'unsat' # ditto
},
'v2.3': {