Skip to content

VirtualBox Control And Snapshot Interlock Source Findings

sergio velderrain edited this page Nov 9, 2026 · 1 revision

VirtualBox Control And Snapshot Interlock: Source Findings

The public VirtualBox Main API and the versioned 7.1.12 SDK reference document the following capabilities. The target host's installed version was not queried in this checkpoint; the SDK's applicability and behavior on each supported host remain separate proof gates.

  • lockMachine documents a write lock for exclusive settings changes, but a Shared request can link to an existing session for VM control, including snapshots. If there is no existing lock, that request can instead obtain a write lock; the actual session type must be inspected. The ISession documentation explicitly permits multiple sessions to control a running VM. Neither a ProjectBuddy UUID lock nor a VirtualBox session lock alone establishes exclusive VM control against other clients.
  • unlockMachine is required for a locked session; its documentation warns that failure to unlock can result in an Aborted machine and lost settings changes. It also says the session need not become Unlocked immediately after the call. Neither condition proves that an already accepted VM operation has stopped; session-type and failure behavior need host-specific proof.
  • takeSnapshot can initiate a live snapshot of a running VM and returns both the UUID of the snapshot to be created and an IProgress object. The snapshot UUID and the progress object's task ID identify different things and must not be interchanged. A successful snapshot becomes the current snapshot; a reserved numbered inventory entry alone is not completion evidence. powerDown also returns an IProgress for its asynchronous operation.
  • IProgress describes asynchronous tasks, a completed flag, and a result code valid only after completion. waitForCompletion(timeout) limits the wait; it does not itself establish that the operation was canceled. The distinct IProgress.timeout property can automatically cancel a cancelable task, and cancel() fails when the task is not cancelable. A cancellation request or a timed-out wait is not terminal evidence without independently confirmed completion and result.
  • findProgressById can find a progress object currently known to VBoxSVC and returns an error for an unknown ID. The API also exposes a progressOperations array. The reviewed documentation does not establish their completeness, retention, VM/operation identity binding, or recovery after a client failure, storage rollback, or server restart. An absent ID or lookup error alone therefore cannot prove that a possibly accepted command did not run or will not complete.
  • IMachine::state and currentSnapshot are observations. The latter can change on take, delete, or restore. The cited APIs do not establish an atomic interlock spanning a state read, a dependent mutation, and other clients. The documentation reviewed also does not establish whether an already accepted operation survives client exit; neither survival nor cancellation may be assumed.

Before dependent mutation, a separately proven resource-side boundary must cover the verified VM, exclude or coordinate relevant competing clients, and account for previously accepted operations throughout the protected interval. Even a successfully completed known task and matching current snapshot are insufficient to exclude a later competing operation. If the boundary, the terminal outcome, or quiescence is unproven, remain UNKNOWN and do not mutate, including by hard poweroff. No control-boundary mechanism is selected by this research.

Clone this wiki locally