-
Notifications
You must be signed in to change notification settings - Fork 0
Home
- Alessandro, Allen, Me
- Weekly discussion
- Set directions for the summer
- We have resources to build a vTPM that might be leveraged
- Ending in September
- Integration of TPM and vTPM
- vTPM uses the TPM
- Functionality of the vTPM {>>vTPM is a superset of TPM<<}
- What should highest priority be for summer?
- Continue verification of the vTPM as is - yes
- Groups in vTPM initialization - yes
- Merge vTPM and TPM specs {>>Whatever that means<<} - maybe
- Migration - no
- Alessandro, Allen, Me
- Catchup
- Alessandro has been working on a model of perfect crypto
- Normal perfect crypto stuff plus synthesis of results from sets {>>cool<<}
- Larry Paulson has papers on his website
- Allen has been working on a system architecture model that
represents communication among entities
- Looking at the StateMonad.pvs theory
- May or may not make sense to use a state monad for representation
- Look for Larry Paulson's security verification papers
- Kestrel, Pete, Daniel, Tim
- Discussion of vTPM functions
- Kestrel, Pete, Daniel, Tim
- Discussion of vTPM functions
- Caller indicates to the domain builder that vTPM cares about a build
- For vTPMs
- For controllers
- Long term name created when vTPM comes up the first time
- The new long term name must be propagated through the system
- Migration will rename as necessary
- Pete, Tim and Daniel from NSA
- Alessandro and Allen from Kestrel
- vTPM Manager and Host Storage
- Vtpm Manager Data and Groups
- vTPM Manager can't do anything with keys until Host Storage is up
- Comes up in stages
- Like Host Storage
- Must wait for data
- Something will cause the vTPM Manager to access its data
- vTPM Manager learns controller hash and ID before it has its data
- This is not a big deal
- Host storage provides no protection initially for vTPM Manager data
- vTPM Manager must encrypt/seal data
- Initial MAC policy governs access
- Host Storage will provide access MAC control later in the process
- Look through Alessandro's notes
- Daniel believes that checking a signature is preferable to unseal
during boot
- Eliminates circular dependencies during boot
- Pete believes that when MAC policy install should trigger a platform
attestation
- Cannot be done locally, but would happen on a guest platform of some kind
- Attestation would occur remotely
- Update description of vTPM Manager to come up in stages - entered
- Look through Alessandro's vTPM data notes - entered
- Look at Ariel's vTPM implementors notes - entered
- Discussing the F2F and what went on
- When is a change accepted?
- What is the process?
- What is Megumi's paper telling us?
- We're not sure yet
- What to the proofs tell us?
- Need to integrate conclusions into the design document
- What is the contribution of formal methods?
- Need to increase our interaction with MITRE
-
Goal: Ensure informative launch-time measurements
- TARA proves that SVP collected launch-time measurements are indicators for theplatform's state (at launch-time)
-
Main Payoffs
- Coponetn specifications must prohibit some behaviors
-
Payoff
- 15 new reuirements to the document {>>need to gather these<<}
Example - Definition of a Regular Hypervisor
- Actions it must take: Algorithms + policies
- Launch the DB
- Follow MAC policy
- Must not allow non-MGR component access to locality 2
- Must not rewquest unsealing K2 or K3
- never reqquest restting or extending protected PCRs
- Never write to protected NVRAM space
- What we gain:
- Precision
- Assurance
- Abstraction
- Families of possible implementation
- Can provide models at multiple abstraction levels
We know that controller IDs must be unique, but we don't know that each entry in the table must have a unique controller ID because multiple TPMs per platform is still allowed.
Tue Dec 17 11:17:32 EST 2013 - Re-added the uniqueness of controller
hashes to the wellFormed? property. This is likey to require
reproving some invarients. Stay tuned for that...
Tue Dec 17 11:22:27 EST 2013 - Added precondition on starting a controller that the domain ID be unique.
Tue Dec 17 11:35:16 EST 2013 - Provision TCC just popped out!
I've weakened the preconditions significantly due to the vTPM measurement not being unique and no explicit requirements for uniqueness of hashes and keys.
The startController function needs to be updated to handle errors.
I tried to avoid this, but no such luck. The TCC asserts that there
should always be a controller ID, but this cannot be guaranteed. So,
let's add some error handling.
14:38 - Added the lifted lfindControllerID and integrated into
startVtpm. Basic type checking passes, but have not checked TCCs.
Will now dive into TCCs from startVtpm that had been giving me fits.
14:47 - WellFormed? does not require controller IDs to be unique,
but it really should as of the last telecon. This does not allow the
TCC associated with startVtpm to go through. This has to be added.
-
Hypervisor starts the Domain Builder from an image on ramdisk
-
Domain Builder starts the vTPM Manager from an image on ramdisk
-
The vTPM Manager infers that this is a provisioning boot, presumably from the absence of:
- encrypted vTPM Manager data
- {~~ wrapped~>sealed ~~} session key K[^0]
- wrapped K_2
-
The vTPM Manager
- Creates its initial {++empty++} data in RAM
- Uses the TPM to generate K_2 wrapped to PCRs 0-4[^4]
- Stores a hash of the wrapped K_2 into the TPM NVRAM[^1]
-
The domain builder starts the SVP controller from an image with access to its schema in ramdisk
-
The domain bulder sends to the vTPM manager the hash of the Controller+Schema and the domain ID of the controller that the vTPM Manager records internally. {++The Controller+Schema hash is unique due to a unique name in the Schema++}
-
The Controller asks the Domain Builder to build/start the Host Storage (from an image in ramdisk).
-
The Controller presumably sees from its Schema that this is a provisioning boot, so it chooses a LTN for the SVP vTPM
- how is this LTN chosen? generated? read from somewhere? is the user prompted at the terminal? is there a terminal running now?
-
The Controller asks the Domain Builder to build/start the SVP vTPM with the chosen LTN.
-
The Domain Builder starts the SVP vTPM from an image in host storage {++along with information needed to start it++}
-
The domain builder sends the vTPM Manager:
- LTN of the vTPM
- Domain ID of the vTPM
- Domain ID of the controller {++VM ID that requested the build++}
- The Hash of the vTPM image + LTN
-
The vTPM Manager creates an entry in the table for the SVP vTPM making a complete entry with the exeception of sealed K_3
-
The vTPM started earlier asks the vTPM manager for its encryption key. As there is no key, the vTPM manger will signal the vTPM that there is none and that this is provisioning boot.
-
The vTPM[^2] {>>Ariel wants this moved to vTPM Manager<<}
- Initializes its own data in RAM
- Generates a new symmetric encyption key K3
- Encrypts its data
- Saves its data to Host Storage
- Sends K_3 to the vTPM Manager
-
The vTPM Manager[^3]
- Recieves K3 from the vTPM
- Uses the domain ID of the vTPM to find the corresponding entry in its table
- Uses the TPM to seal K3 to PCR5 & PCR6 that contain the hash of the vTPM Image and LTN and the hash of the controller image and Schema
- Updates the table entry with the sealed K3
[^0]:Sealing only occurs on platform and includes information of state. Binding does not allow PCR constraints and can be done off platform. [^1]:Owner creates an area in NVRAM that is writable only by good software. This is where the hash is stored. [^2]:The generation of K3, encryption and saving of data, and sending of K3 to the vTPM Manager is the normal process that happens whenever the non-volatile vTPM data {~~changes~>is stored~~} [^3]:This step is the normal process by which the vTPM manager updates the K3 of a vTPM [^4]:Wrapping/Sealing does not occur with respect to the current PCRs. The command specifies PCR numbers and values when wrapping/sealing.
- How can the wrapped K_2 be generated without having PCRs in the right state in the TPM? Do not seal with SRK, but with a key generated with SRK as parent. Still, how does one specify the values of the PCRs for the seal? {++PCR values for seals/wraps are not obtained from the TPM, but provided at the command line.++}
- There is a thing called preprovisioning. Where does it stop?
- What is measured when the vTPM starts? vTPM or vTPM+LTN?
- Schema contains a unique name for the platform. Platform+Schema hash is unique.
- Schema contains the vTPM name to start he vTPM. vTPM name might be a uuid.
- vTPM Name is unique among the platforms it may migrate to. Daniel believes the global name can be transient. Managed by migration agent.
- NVRAM must be protected so only the owner can update it.
- Different platforms would specify different locations in NVRAM.
- Controller+Schema hash is unique because the name in the schema is unique. It is not cryptographically important.
- Discuss removing K_2 at the F2F.
Pulled the well-formedness check for controller entries out of the state check for the time being. Added the wellFormed? predicate subtype to the input and output state of startController.
Re-verified TCCs with the wellFormed? predicate subtype added to the input and output state of startController.
Defined and proved a simple invariant over controller startup. Simply checks that controller startup does not impact the vTPM part of the vTPM manager state and the added controller dom ID is in the table after execution.
startVtpm(lnt:LTN_vtpm
, vdom,cdom:ID\_dom
, hvtpm:HASH
, s:(wellFormed?)) : wellFormed?=
%% Find the controller hash
%% Create dynamic info
%% Update entry with (# Static Info, Dynamic Info #)
Need the uniqueness of the controller before one of the TCCs will pop out for startVtpm. Not happy about that, but it should be fine.
Diving into re-verifying everything with the new storage of controller hashes. This is what needs to happen:
- Add controller hashes to the controller table with appropriate error checking and handing
- Integrate the controller table into vTPM startup
- Verify vTPM startup invariants and types
Performed major surgery on the vTPM specification. Retargetted functions to operate over a new state that contains a controller table mapping domain IDs to hashes.
I have not updated the functions to add the controller hash properly to the vTPM table. This is yet to be done.
Discussing uniqueness of the vTPM hash and the controller hash.
- Are they unique?
- Over what domain are they unique?
The vTPM hash may not be unique because the vTPM's data is not loaded when it is hashed.
Add a controller hash table with mappings from cotroller domain ID to controller hash that are used to populate the existing table.
Steps through vTPM boot:
- DB starts controller, passes hash and domID to vTPM Manager
- vTPM Manager stores hash and domID for future use
- Controller requests start of the vTPM with LTN
- DB starts the vTPM and passes controller domID, vTPM domID, vTPM LTN, and vTPM hash to the vTPM manager
- vTPM manager populates the vTPM
- Find the LTN entry
- Add vTPM domID and vTPM hash to vTPM manager table entry
- Find controller entry in controller table
- Add controller hash to vTPM manager table entry
Cannot start multiple instances of the same vTPM LTN because there is only one entry associated with each LTN in the vTPM Manager table.
Looking at what starting up a vTPM means and what has to happen. Preconditions:
- The LTN associated with the vTPM must exist in the vTPM Manager Table Before the vTPM can start. Checked
- The LTN associated with the vTPM must not be started already Checked
- The key must unseal given the controller and vTPM hashes in PCR 5 and PCR 6
Postconditions:
- The entry associated with the LTN has an associated domain ID and is populated with hashes.
- k_D does not change from the value originally in the table.
- Pulled the k_D parameter from the startup function. It is not needed as k_D does not change.
- Removed the platform (controller) ID from the startVtpm function
- Added check for valid domain ID alread in table
- The vTPM hash need not be unique, but the controller hash must be
When a vTPM starts it must uniquely identify its associated table entry. The hash of the vTPM need not be unique in the current model. The hash of the platform does need to be unique, but there may be more than one vTPM associated with it. Really, the only thing in the table that must be unique is the LTN of the vTPM.
Controller - Hash is unique vTPM - Hash is not unique LTN vTPM - unique, but not included in the hash
A controller can build two copies of the same vTPM by providing the same LTN. Is this a problem?
A controller cannot build a duplicate of a vTPM whose data is sealed to the unique hash of the controller. Thus, another controller cannot start a second copy of a vTPM it does not already have permission to start via the controller hash.