úÎjºf•5      !"#$%&'()*+,-./01234@This method determines the observational power of the attacker. C Attackers are then capable to break the abstraction of the ! security monads in module Sec and SecIO for security levels  below or equal than s. :This method determines that information at security level s can flow to security level s'. )This type represents pure values of type a at confidentiality level s. 56!Assign the confidentiality level s to a value of type a. +Raise the confidentiality level of values. !Break the abstraction provide by . #It is used only in trustworthy code. 7=Internal function, not exported. For type-checking purposes. -Reveal values that the attacker can observe. 5675567,5It defines a socket address at confidentiality level s. 8 >Locations that represent network communications via sockets. JLocation that represents the screen-keyword. Here, we can choose between U a) The attacker is on the screen-keyword, which implies that when taking input X from the screen has an effect -- the attacker can see when the input is required. I Therefore, we need to implement taking input from the keyword using 9. O b) The attacker is not on the screen-keyword. In this case, we implement  reading using :". We choose option a) as a model. &Locations that represent references. "Locations that represent files ;?Introduce safe read and write operations for locations of type   t s a. 4 This class acts as a wrapper for the type class <. 9JIt provides a secure read operation when reading values might be visible 7 for the attacker (from inside of the program). S For example, reading from a channel in a network communication changes the U buffer pointer for that channel, which can be exploited to leak information. :\It provides a secure read operation when reading values is not observable by the attacker. T For example, reading from references does not produce any observable effect. =&It provides a secure write operation. <LIntroduce the underlining operations for reading and writing values of type a provided  the type t. >? Represent secure locations. ] This data type is internally used to easily introduce new side-effects into this module.  Type t@ is the raw type needed to perform side-effects. For instance,  t is @ for files and A a for references. Type s& is the confidentiality level of the  location. Type a- is the type of values written and read form t. 7This type represents secure side-effect computations. I These computations perform side-effects at security level, at least, s and return  a value of type a' with confidentiality level, at least, s. BGLift a pure confidential value into a secure side-effect computation. Execute secure computations. _Safely downgrade the security level indicating the side-effects performed by the computation. C=Internal function, not exported. For type-checking purposes. "Break the abstraction provided by '. It is used only in trustworthy code! !Secure read operation for files. #Secure write operation for files. 8Creation of files is only allowed by trustworhty code. &Observe that by creating a file, the ;confidentiality level of its content is being established. ATherefore, the attacker can create a public file using the name %of a secret file and just read it! | &Secure read operation for references. 'Secure write operation for references. =Secure creation of a reference. We assume that the attacker b has no manner to observe the side-effect of creating a reference from inside of the program, p for example, by inspecting the amount of free memory. At the moment, there are no such functions inside of  the monad _. Nevertheless, if there is a consideration of include, for instance, a function that returns H the amount of free memory in the program, then the function type of  needs  to be changed. 0It sets the security level of the standard input/output (usually the keyboard/ screen). 'To be used only by trustworthy code. | Secure input from the keyword. Secure output to the screen. Secure output to the screen. @It is a derived operation for reading from files (legacy code). @It is a derived operation for writing into files (legacy code).  Wrapper for D. !Assing a port to the E$ sockets. Port numbers are public. ")Create a socket at confidentiality level s2. The creation has no visible side-effects, e.g. L sockets cannot be compared. This function is essentially a wrapper for F. #$-Return if a socket is bound to some address. % Wrapper for G. &$Secure read operation for sockets. '%Secure write operation for sockets. (*Connects to a socket. It is a wrapper for H. )<Determines a given socket is connected. It is a wrapper for I. ,8 ;9:=<>? BC !"#$%&'(),88 ;9:=9:=<>?>? BBC !"#$%&'() *Used by 0. J+Used by /4. It represents computations that close flow locks. ,Used by /3. It represents computations that open flow locks. -Create an escape hatch. .BLimit the number of times that an escape hatch can be applied by # a single run of the program. /:This function associates a flow lock to an escape hatch.  Then, the escape hatch ? can be successfully applied when the flow lock is open. G The escape hatch cannot by applied after closing the flock lock. 0AThis function allows to an escape hatch to be applied only when m the running code can be certified with some authority. The certification process is just to show that 3 the code has access to a constructor of type sh. 16Certify that a piece of code have certain authority. *+,-./01*+,-./012  !"#$%&'()*+,-./012     !"#$%&'(),+*1 -./0 2LData type representing the security level associated to secret information. K3LData type representing the security level associated to public information. L4!The attacker is at the terminal. M'For internal use. It is not exported. N&The attacker can observe public data. O&Public information can become secret. P7Information can flow among entities of the same level. 234324234$  !"#$%&'()*1$     !"#$%&'()*1Q      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJHKLMNOPQORSOPTOPUOPVOPW2:;XYZ[\ seclib-0.7SecLib.TrustworthySecLib.LatticeLHSecLib.Lattice SecLib.Sec SecLib.SecIOSecLib.DeclassificationSecLib.UntrustworthyAttackerobserveLesslessSecuprevealpublic SecSockAddr SecSocketScreenRefFileLocMkLocSecIOvaluerunplugrevealIO readFileSecIOwriteFileSecIOmkFile readRefSecIO writeRefSecIO newIORefSecIOmkScreen getLineSecIO putStrSecIO putStrLnSecIOs_reads_writeinet_addrSecIOportInet socketSecIObindSocketSecIO sIsBoundSecIO acceptSecIO recvSecIO sendSecIO connectSecIOsIsConnectedSecIO AuthorityCloseOpenhatchntimesflockdlmcertifyHLscrMkSecsec unSecType MkSockAddreffectful_readeffectless_readSecureRW UnsecureRWeffectful_write unsec_write unsec_readbaseGHC.IOFilePath GHC.IORefIORefMkSecIO unSecIOTypenetwork-2.3.0.4Network.Socket inet_addrNetwork.Socket.InternalAF_INETsocketacceptconnect sIsConnectedunLoc $fAttackerL$fLessLH$fLessaa