No comment

Author: xaionaro@dx.center

.gitignore

@@ -8,3 +8,5 @@
 *.prof
 /build/
 *.exe
+/.lake
+proofs/.lake

Makefile

@@ -1,5 +1,5 @@
 .PHONY: specs generate cli readme test e2e e2e-bindercli vet build lint clean \
-       bindercli list-commands check-generated release
+       bindercli list-commands check-generated release proofs difftest
 
 # Generated top-level directories.
 GENERATED_DIRS := android com fuzztest libgui_test_server parcelables src
@@ -31,6 +31,16 @@ cli: specs
 readme: specs
 	go run ./tools/cmd/spec2readme -specs specs/ -output README.md
 
+# --- Proofs ---
+
+# Build Lean 4 proofs (requires elan/lake toolchain).
+proofs:
+	cd proofs && lake build
+
+# Run differential tests comparing Go against Lean oracle.
+difftest: proofs
+	go test -v ./tests/differential/
+
 # --- Testing ---
 
 # Run unit tests.

binder/config.go

@@ -0,0 +1,15 @@
+package binder
+
+// Config holds Transport configuration.
+type Config struct {
+	MaxThreads uint32
+	MapSize    uint32
+}
+
+// DefaultConfig returns the default transport configuration.
+func DefaultConfig() Config {
+	return Config{
+		MaxThreads: 0,
+		MapSize:    1024*1024 - 2*4096, // 1MB - 2*PAGE_SIZE
+	}
+}

binder/option.go

@@ -5,20 +5,6 @@ type Option interface {
 	apply(*Config)
 }
 
-// Config holds Transport configuration.
-type Config struct {
-	MaxThreads uint32
-	MapSize    uint32
-}
-
-// DefaultConfig returns the default transport configuration.
-func DefaultConfig() Config {
-	return Config{
-		MaxThreads: 0,
-		MapSize:    1024*1024 - 2*4096, // 1MB - 2*PAGE_SIZE
-	}
-}
-
 // Options is a slice of Option.
 type Options []Option
 

binder/proxy_binder.go

@@ -61,6 +61,9 @@ func (b *ProxyBinder) LinkToDeath(
 	ctx context.Context,
 	recipient DeathRecipient,
 ) (_err error) {
+	logger.Tracef(ctx, "LinkToDeath(handle=%d)", b.handle)
+	defer func() { logger.Tracef(ctx, "/LinkToDeath: %v", _err) }()
+
 	return b.transport.RequestDeathNotification(ctx, b.handle, recipient)
 }
 
@@ -69,6 +72,9 @@ func (b *ProxyBinder) UnlinkToDeath(
 	ctx context.Context,
 	recipient DeathRecipient,
 ) (_err error) {
+	logger.Tracef(ctx, "UnlinkToDeath(handle=%d)", b.handle)
+	defer func() { logger.Tracef(ctx, "/UnlinkToDeath: %v", _err) }()
+
 	return b.transport.ClearDeathNotification(ctx, b.handle, recipient)
 }
 

binder/status.go

@@ -37,7 +37,11 @@ func ReadStatus(p *parcel.Parcel) error {
 
 	if traceSize > 0 {
 		// Skip the remote stack trace string.
-		_, _ = p.ReadString16()
+		// Propagate the error: a truncated trace corrupts the read
+		// position, causing subsequent fields to read garbage.
+		if _, err := p.ReadString16(); err != nil {
+			return fmt.Errorf("binder: reading status trace string: %w", err)
+		}
 	}
 
 	statusErr := &aidlerrors.StatusError{

binder/status_test.go

@@ -1,6 +1,7 @@
 package binder
 
 import (
+	"errors"
 	"fmt"
 	"testing"
 
@@ -84,3 +85,27 @@ func TestWriteStatusGenericError_ReadStatus(t *testing.T) {
 	assert.Equal(t, aidlerrors.ExceptionTransactionFailed, statusErr.Exception)
 	assert.Equal(t, "something went wrong", statusErr.Message)
 }
+
+func TestReadStatus_TruncatedTraceString(t *testing.T) {
+	// Build a parcel that claims traceSize > 0 but contains no trace
+	// string data. Before the fix, ReadString16 error was silently
+	// discarded, corrupting the read position so that the subsequent
+	// ReadInt32 for ServiceSpecificCode would read garbage instead of
+	// returning an error.
+	p := parcel.New()
+	p.WriteInt32(int32(aidlerrors.ExceptionServiceSpecific)) // exception code
+	p.WriteString16("service error")                         // message
+	p.WriteInt32(1)                                          // traceSize > 0 (claims a trace exists)
+	// Deliberately omit the trace string data — parcel is truncated here.
+
+	p.SetPosition(0)
+
+	err := ReadStatus(p)
+	require.Error(t, err)
+	assert.Contains(t, err.Error(), "reading status trace string")
+
+	// Must NOT be a StatusError with garbage ServiceSpecificCode.
+	var statusErr *aidlerrors.StatusError
+	assert.False(t, errors.As(err, &statusErr),
+		"truncated parcel must not produce a StatusError with garbage fields")
+}

binder/stub_binder.go

@@ -103,8 +103,8 @@ func (s *StubBinder) BinderPtr() uintptr {
 	return uintptr(unsafe.Pointer(s.weakRef))
 }
 
-// Transport returns nil for unregistered stubs; after
-// RegisterWithTransport it returns the transport that was used.
+// Transport returns nil — StubBinder does not implement VersionAwareTransport
+// lookup. Use the transport directly instead.
 func (s *StubBinder) Transport() VersionAwareTransport {
 	return nil
 }

binder/transaction.go

@@ -16,18 +16,3 @@ const (
 	InterfaceTransaction TransactionCode = ('_' << 24) | ('N' << 16) | ('T' << 8) | 'F'
 	SyspropsTransaction  TransactionCode = ('_' << 24) | ('S' << 16) | ('P' << 8) | 'R'
 )
-
-// TransactionFlags control transaction behavior.
-type TransactionFlags uint32
-
-const (
-	FlagOneway              TransactionFlags = 0x00000001
-	FlagCollectNotedAppOps  TransactionFlags = 0x00000002
-	// FlagAcceptFDs tells the binder kernel that this process can receive
-	// file descriptors in the reply. Without this flag, the kernel rejects
-	// replies containing FDs with BR_FAILED_REPLY. Android's
-	// IPCThreadState::transact() always sets this flag.
-	FlagAcceptFDs           TransactionFlags = 0x00000010
-	FlagClearBuf            TransactionFlags = 0x00000020
-	FlagPrivateVendor       TransactionFlags = 0x10000000
-)

binder/transaction_flags.go

@@ -0,0 +1,16 @@
+package binder
+
+// TransactionFlags control transaction behavior.
+type TransactionFlags uint32
+
+const (
+	FlagOneway              TransactionFlags = 0x00000001
+	FlagCollectNotedAppOps  TransactionFlags = 0x00000002
+	// FlagAcceptFDs tells the binder kernel that this process can receive
+	// file descriptors in the reply. Without this flag, the kernel rejects
+	// replies containing FDs with BR_FAILED_REPLY. Android's
+	// IPCThreadState::transact() always sets this flag.
+	FlagAcceptFDs           TransactionFlags = 0x00000010
+	FlagClearBuf            TransactionFlags = 0x00000020
+	FlagPrivateVendor       TransactionFlags = 0x10000000
+)