-
Notifications
You must be signed in to change notification settings - Fork 0
Adam Petz Log
ampetz edited this page Jul 16, 2014
·
16 revisions
My working definition of a Monad:
Two things happen simultaneously during the execution of a monadic bind operation:
-
The pure calculations inside the monad deliver their result to the next composed computation(monad), where the result can optionally be used in subsequent pure calculations. This is exactly the same as pure function composition, except that it is happening inside a monad.
-
The monad performs some task specific to its computational context. Examples: Maybe can introduce failure, Error can trigger error exceptions, list([]) propogates non-determinism, IO performs side effects(related to input/output), State-"threading state through a series of functions." It knows about its mutable structures(simulated mutable) and can alter them(as explicitly defined by the monad, implicitly performed upon bind).
The implicit "magic" that happens upon a bind is defined for each Monad instance in its overloaded >== operator implementation. This removes the Monad-specific clutter from the code, turning the focus to the algorithm, and also making the algorithm more extensible(can be wrapped in Monads to extend functionality).
Potentially useful Haskell libraries for protocol demos
Crypto package -> Codec.Encryption.RSA (for Asymmetric Key)
Nonce package -> Crypto.Nonce (generating nonces)
Thoughts on protocol demo 1: Need to nail down what actions should stay at the protocol layer, and what we can push to other layers.
- Do we want our protocol to interact directly with Crypto libraries?(Probably not. We may want to create a general interface to crypto libraries so that we can pass general parameters and let our "crypto layer" do the dirty bits.)
- Serialization is another issue. Our protocol layer should not be concerned with serialization/de-serialization, but it needs to happen somewhere before we hand off data to the communication layer.
Potentially useful language features of Erlang:
- Processes maintain hidden state(i.e. a message mailbox). Does this motivate us using the State monad to simulate this feature in our EDSL in Haskell?
- Asynchronous communication:
-Each message/action is self-contained(Our protocol semantics are distinct from their execution environment: promotes communication in a heterogenous environment, allows protocol to be abstract).
-Scales well to large number of VM interactions(maybe less busy waiting: reactive programs). -No explicit reply message is necessarily mandated/expected by caller(but we still need to provide some verification that the message acted appropriately). - Explicit address communication: Each Process(function, computation) has a unique PID that other processes must use(hence, have) in order to communicate with it. Will help with privacy/disclosure. "Every communication is explicit, traceable and safe."
- Code is compiled into bytecode and runs on a virtual machine.
- Actor model -inherently concurrent -control structures as patterns of passing messages -ability to create new actors, send messages to delegate services. Each receiver will "know" how to act appropriately in response to message(or it won't, but will exit in an appropriate manner, possibly propagating the message elsewhere where it might be handled).
- "Selective Receives" feature allows processes to only handle messages that they care about(and by priority). Processes can optionally ignore un-useful messages, accumulate them, or resend.
- Linking processes such that if one "dies", those linked to it "die" as well(dying may simply re-start the process or re-delegate it: One approach is to have a "supervisor" process that is in charge of re-starting dead processes). This linking mechanism could be a useful self-protection mechanism for a fail-safe protocol. "Monitors" are alternate links that do not create hard dependencies(monitors can be stacked and removed(un-linked) arbitrarily, and are unidirectional(whereas normal links cannot, and are bidirectional) ).
- Distinction between "process" and "function": Different processes can use the same function, but each process uses the function with its own context.(i.e. If we call the link/1 function from within another function, it links the CURRENT process to the one specified by the supplied PID argument.). This feature supports our notion of a common protocol interface(functions) as a utility for multiple instances of our executable protocol(processes).
- Ability to update code while it is running("hot code loading"): extensibility of our language of trust(might be useful if desired security properties change, or our protocol implementation itself needs modification/customization).
- Design idiom: First, separate components into processes, then specify 1) what each process should do and 2) what each process should communicate.
- "Message References" are built-in and are an established idiom: Similar to the ubiquitous use of nonces in our protocol.
- Generic Module access that depends on context(i.e. the ?MODULE macro that loads the module with that name in its particular context. This allows module variations to exist to support the diverse measurement/attestation environments that execute the protocol: module is context specific, may use local utilities, etc.) ).
- Separate handling of synchronous and asynchronous calls(in a generic fashion).
- Messages matched based on tags called "atoms"(basically an identifier). Might be natural to simulate this feature by using types in Haskell, with the added advantage of verification capability.
Cloud Haskell Notes
- Towards Haskell in the Cloud(Simon Peyton-Jones et. al) -"We choose this model(Erlang message-passing/actor model) because it makes the costs of communication apparent, and because it makes a concurrent process a natural unit of failure: since processes do not share data, the data of one process cannot be contaminated by a fault in another" -Has all the benefits of the Erlang style, but with purity, types, and monads on top. Cloud Haskell also differs from Erlang in that it supports shared-memory concurrency WITHIN A SINGLE PROCESS.(Importantly, mechanisms specific to shared-memory concurrency cannot be inadvertently used between remote systems: by restricting them from being Serializable). -A "node" is Cloud Haskell's "unit of location". NodeID is its unique identifier that contains an IP address that can be used to communicate with the node.
"Prudent Engineering Practice for CryptoGraphic Protocols"(Abadi and Needham) Notes
- We recommend the use of a logical notation in generating and describing protocols...Establishing the correspondence between the logical protocol and its concrete implementation can be a simple mater of parsing… -“A Logic of Authentication” M. Burrows, M. Abadi, and R.M. Needham.
- Isolating verifiable components: “authentication of any message in the protocol depends only on information contained in the message itself or already in the possession of the recipient”
- Difference between secrecy, integrity, and authenticity (and how different protocol features promote each).
- Note: For a protocol, in general, There is nothing in the environment to guarantee that messages are made in numerical order by the principals indicated, received in numerical order OR AT ALL by the principals indicated, or received solely by the principals indicated. IF ASSURANCE IS NEEDED ABOUT ANY OF THESE MATTERS IT MUST BE PROVIDED AS PART OF THE FUNCTION OF THE PROTOCOL.
- Timestamps are a ubiquitous element of protocols. They are often bound to messages: We could provide these in messages from the Measurer to give appropriate durations during which measurements (that indicate software state) can be expected to stay valid. However, heavy reliance on synchronized time servers opens up a large class of attacks, and adds complexity that may hinder verification efforts. Often, strategies involving nonce-enhanced transactions can be used to avoid timestamps.
- Encryption can contribute to the semantics of a message (encryption is an explicit contributor to the meaning of each message to which it is applied).
- Technique: A principal shows that a key is known by encrypting a null message or a timestamp.
- Notion: T for timestamps, L for lifetimes
- Demo2: Keep new(next) nonce generator as part of the state between calls to the measurer.
- Order of signing/encrypting is critical(Principle 5: Order tells whether or not the receiver can be assured that the sender has “seen” portions of the content that it sends.)
- Protocols that rely on synchronized clocks must be accompanied by protocols to access time servers. These protocols cannot themselves rely on synchronized clocks (this, and related protocol concepts sound like excellent applications for a monad: Preventing execution in some sort of dangerous computational context-realizing these restrictions with a monad may lend itself to clearer/easier verification?), but they can rely either on random nonces or on predictable nonces.
Demo 2 Thoughts
- Demo 2 should extend Demo 1 to incorporate a "looping mechanism"(sequencing mechanism?) to drive interaction between the Attestation agent and the Measurer(handle MULTIPLE measurement requests and responses). -Looping in Haskell?(Possibly useful functions/libraries: whileM, untilM(Control.Monad.Loops), Control.Monad.Trans.Loop) -How can we use Monads and Monad Transformers to get the sequential properties we want?
- Questions: how do we 1) request, 2) initiate measurement, 3) store intermediate results(what does our "state" data structure look like, if we use a state monad-like approach), 4) terminate, 5) aggregate, 6) sign? 7) respond 8) evaluate
- Interesting ideas to explore:
-Use Writer monad(transformer?) to log a trace of all communication/action(at least for debugging, but possibly to aid in verification). -Use Reader monad(transformer?) to maintain copies of crypto keys(questions: Is this even necessary?-why not just have a local key file. How do we get the keys into the Monad initially?) -Maintain the next random generator for nonces internally in our protocol execution Monad(for subsequent nonce creation). -Send the combination(hash or simply concatenation/pairing) of the Appraiser-generated nonce and the Attestation-generated nonce to the Measurer for each measurement request.
Demo 2: Thoughts on Measurement Data and Evaluation
- Consider order of measurement and order of evaluation(Both for debugging and in production). Ultimately, we will need to define each Appraiser's internal standards regarding the evidence it evaluates. Thus, we should probably have the Appraiser record the Boolean result of each sub-evaluation of the evidence it receives in order to have a fine-grained concept of what parts of the message it can trust, and which pieces of evidence match its expectations.
- Thus, even though a sub-evaluation may partially condemn the target, evaluation should continue on the rest of the response message.
- How do we map Evidence Descriptors to the data structures that they describe? (Should all evidence be of a uniform format? How do we account for the diversity of measurement types?)
Demo 2: Potential primitive operations that our protocol should support
- generateNonce: Maybe use state monad-like strategy to maintain the next generator upon subsequent nonce generations.
- mungeData(packData?): May be polymorphic on the type of data it munges(packs). Purpose is to define a UNIFORM way to combine data into a single blob so that it may be hashed over, or operated on in some way as a whole. Uniformity is important since two different principles may need to compare hashes over the same data(thus assuming that its data is munged in the same fashion). QUESTION: Where does this "munging" happen? Can Measurement agent munge before sending it back? If so, we may eliminate some complexity(although we still need to separate and evaluate individual measurements: pre-munging might make this harder).
- hash
- sign(for authenticity)
- verify(checks signature)
- encrypt(for secrecy)
- decrypt(undoes encryption)
- sendRequest
- receiveResponse
- sequenceActions
- retryActionGroup
- verifyMeasurement, verifyMechanism(Differentiate between measurement results and infrastructure trustworthiness results)