This commit is contained in:
Rasmus Lerchedahl Petersen 2023-03-24 13:32:25 +01:00
Родитель 8ea4878f7a
Коммит 3c407eaa23
1 изменённых файлов: 6 добавлений и 11 удалений

Просмотреть файл

@ -4,21 +4,16 @@ import TlsLibraryModel
/**
* Configuration to determine the state of a context being used to create
* a connection. There is one configuration for each pair of `TlsLibrary` and `ProtocolVersion`,
* such that a single configuration only tracks contexts where a specific `ProtocolVersion` is allowed.
* a connection. The configuration uses a flow state to track the `TlsLibrary`
* and the insecure `ProtocolVersion`s that are allowed.
*
* The state is in terms of whether a specific protocol is allowed. This is
* either true or false when the context is created and can then be modified
* later by either restricting or unrestricting the protocol (see the predicates
* `isRestriction` and `isUnrestriction`).
* later by either restricting or unrestricting the protocol (see the predicate
* `isAdditionalFlowStep`).
*
* Since we are interested in the final state, we want the flow to start from
* the last unrestriction, so we disallow flow into unrestrictions. We also
* model the creation as an unrestriction of everything it allows, to account
* for the common case where the creation plays the role of "last unrestriction".
*
* Since we really want "the last unrestriction, not nullified by a restriction",
* we also disallow flow into restrictions.
* The state is represented as a bit vector, where each bit corresponds to a
* protocol version. The bit is set if the protocol is allowed.
*/
module InsecureContextConfiguration implements DataFlow::StateConfigSig {
private newtype TFlowState =