⚡

类型化汇编语言Skill typed-assembly-language

类型化汇编语言是一种用于验证汇编级别代码类型安全的技术，通过为机器指令添加类型系统，确保内存访问安全、控制流正确，适用于编译器验证、证明携带代码和可信系统。关键词：类型化汇编语言，汇编语言，类型安全，内存安全，验证编译，证明携带代码。

操作系统 0 次安装 0 次浏览 更新于 3/13/2026

name: 类型化汇编语言 description: ‘使用类型化汇编语言验证低级代码。适用场景：(1) 验证编译，(2) 证明携带代码，(3) 可信系统。’ version: 1.0.0 tags:

  • 编译器
  • 类型化汇编
  • 低级
  • 验证 difficulty: 高级 languages:
  • 汇编
  • coq dependencies:
  • 类型检查器生成器

类型化汇编语言

使用类型化汇编语言 (TAL) 验证低级代码。

适用场景

  • 验证编译
  • 证明携带代码
  • 低级验证
  • 可信系统

技能功能

  1. 类型化低级代码 - 将寄存器、内存类型化
  2. 验证安全性 - 类型保持
  3. 处理调用 - 栈和调用约定
  4. 证明属性 - 使用霍尔逻辑

使用方法

  1. 定义机器模型（寄存器、内存、指令集）
  2. 为寄存器和代码指针分配 TAL 类型
  3. 检查每个指令更新类型环境是否合理
  4. 验证控制流汇合和调用约定不变性

核心理论

TAL 类型：
  int              : 整数
  ptr(τ)           : 指向 τ 的指针
  arr(τ, n)       : τ 类型长度为 n 的数组  
  code(Γ ⊢ τ)     : 带类型的代码指针
  tuple(τ₁...τₙ)  : 元组

类型规则：
  r : τ            : 寄存器具有类型 τ
  ρ ⊢ m : τ        : 内存地址 ρ 具有类型 τ
  ⊢ i : τ          : 指令具有类型 τ

实现

from dataclasses import dataclass
from typing import Dict, List, Set, Optional

@dataclass
class TALType:
    """TAL 类型"""
    pass

@dataclass
class TInt(TALType):
    """整数类型"""
    pass

@dataclass
class TPtr(TALType):
    """指针类型"""
    elem: TALType

@dataclass
class TCode(TALType):
    """代码指针类型"""
    arg_types: List[TALType]
    ret_type: TALType

@dataclass
class TTuple(TALType):
    """元组类型"""
    types: List[TALType]

@dataclass
class TArray(TALType):
    """数组类型"""
    elem: TALType
    length: int

# 寄存器文件
RegFile = Dict[str, TALType]

# 内存：地址 -> 类型
Memory = Dict[int, TALType]

@dataclass
class TALInstruction:
    """TAL 指令"""
    pass

@dataclass
class Mov(TALInstruction):
    """mov dst, src"""
    dst: str
    src: str

@dataclass
class Add(TALInstruction):
    """add dst, src1, src2"""
    dst: str
    src1: str
    src2: str

@dataclass
class Load(TALInstruction):
    """load dst, [src + offset]"""
    dst: str
    src: str
    offset: int

@dataclass
class Store(TALInstruction):
    """store [dst + offset], src"""
    dst: str
    offset: int
    src: str

@dataclass
class Call(TALInstruction):
    """call addr"""
    target: str

@dataclass
class Ret(TALInstruction):
    """ret"""
    pass

@dataclass
class Branch(TALInstruction):
    """beq r, label"""
    cond: str
    target: str

class TALChecker:
    """TAL 类型检查器"""
    
    def __init__(self):
        self.registers: RegFile = {}
        self.memory: Memory = {}
        self.code_types: Dict[str, TCode] = {}
    
    def check_instruction(self, instr: TALInstruction, 
                         env: RegFile) -> RegFile:
        """检查指令，返回新的寄存器类型"""
        
        match instr:
            case Mov(dst, src):
                # 复制类型
                if src in env:
                    return {**env, dst: env[src]}
                raise TypeError(f"未知寄存器: {src}")
            
            case Add(dst, src1, src2):
                # 整数加法
                if (src1 in env and src2 in env and
                    isinstance(env[src1], TInt) and
                    isinstance(env[src2], TInt)):
                    return {**env, dst: TInt()}
                raise TypeError("加法中使用非整数")
            
            case Load(dst, src, offset):
                # 从内存加载
                if src in env and isinstance(env[src], TPtr):
                    ptr_ty = env[src]
                    addr_type = self.memory.get(offset, ptr_ty.elem)
                    return {**env, dst: addr_type}
                raise TypeError("无效加载")
            
            case Store(dst, offset, src):
                # 存储到内存
                if dst in env and src in env:
                    self.memory[offset] = env[src]
                    return env
                raise TypeError("无效存储")
            
            case Call(target):
                # 检查代码类型
                if target in self.code_types:
                    # 为简化，假设函数返回单位类型
                    return {**env}
                raise TypeError(f"未知函数: {target}")
            
            case Ret():
                # 返回，恢复调用者状态
                return {}
            
            case Branch(cond, target):
                # 检查条件是布尔值/整数
                if cond in env:
                    return env
                raise TypeError(f"未知寄存器: {cond}")
        
        return env

堆分配

class TALHeap:
    """带堆分配的 TAL"""
    
    def __init__(self):
        self.heap: Dict[int, tuple] = {}
        self.next_addr = 0x1000
    
    def malloc(self, size: int, layout: TTuple) -> TPtr:
        """分配堆对象"""
        
        addr = self.next_addr
        self.next_addr += size
        
        # 存储布局信息
        self.heap[addr] = ('obj', layout)
        
        return TPtr(layout)
    
    def check_heap_access(self, ptr: TPtr, offset: int) -> TALType:
        """检查堆访问类型"""
        
        if isinstance(ptr.elem, TTuple):
            # 检查字段类型
            field_idx = offset // 8  # 假设 8 字节字段
            if field_idx < len(ptr.elem.types):
                return ptr.elem.types[field_idx]
        
        raise TypeError("无效堆访问")

验证编译

class VerifiedCompiler:
    """编译和验证"""
    
    def __init__(self):
        self.tal_checker = TALChecker()
    
    def compile_and_verify(self, high_level: 'Expr') -> bool:
        """
        编译高级语言到 TAL 并验证
        """
        
        # 1. 编译到中间表示
        ir = self.compile_to_ir(high_level)
        
        # 2. 生成 TAL 代码
        tal_code = self.generate_tal(ir)
        
        # 3. 添加类型注释
        typed_tal = self.annotate_types(tal_code)
        
        # 4. 验证类型
        return self.verify(typed_tal)
    
    def verify(self, tal_code: List[TALInstruction]) -> bool:
        """验证 TAL 类型安全"""
        
        env = {}
        
        for instr in tal_code:
            try:
                env = self.tal_checker.check_instruction(instr, env)
            except TypeError as e:
                print(f"类型错误: {e}")
                return False
        
        return True

证明携带代码

class PCChecker:
    """证明携带代码验证"""
    
    def __init__(self):
        self.policy = SafetyPolicy()
    
    def verify_pcc(self, code: bytes, proof: bytes) -> bool:
        """
        验证证明携带代码
        """
        
        # 1. 提取安全策略
        policy = self.extract_policy(code)
        
        # 2. 验证证明
        proof_valid = self.verify_proof(policy, proof)
        
        if not proof_valid:
            return False
        
        # 3. 执行可信代码
        return self.execute_trusted(code)
    
    def extract_policy(self, code: bytes) -> SafetyPolicy:
        """从代码中提取安全策略"""
        
        # 读取类型注释
        # 构建策略
        return self.policy
    
    def verify_proof(self, policy: SafetyPolicy, 
                    proof: bytes) -> bool:
        """验证证明尊重策略"""
        
        # 简单：检查证明格式
        # 真实：使用证明助手验证
        return len(proof) > 0

核心概念

概念 描述
类型保持 良好类型化 → 良好类型化
内存安全 无无效访问
控制流 调用/返回类型化
子类型 指针子类型

属性

属性 描述
类型安全 无类型错误
内存安全 边界检查
控制安全 有效调用/返回
非干涉 无信息泄露

提示

  • 使用静态验证
  • 检查所有路径
  • 处理异常
  • 考虑宽松模型

相关技能

  • coq-proof-assistant - 证明助手
  • ssa-constructor - SSA 形式
  • garbage-collector-implementer - 运行时

研究工具与成果

实际世界 TAL 系统：

工具 为何重要
TAL/T 类型化汇编语言
SPARC TAL SPARC 架构
Cool 验证编译器
CertiCoq 验证 Coq 编译器

关键系统

  • Coq：证明助手
  • CakeML：验证编译器

研究前沿

当前 TAL 研究：

方向 关键论文 挑战
验证 “Verified Compilation” 端到端
PCC “Proof-carrying Code” 证明

热门话题

  1. Wasm 验证：WebAssembly 类型化
  2. RISC-V TAL：新架构

实现陷阱

常见 TAL 错误：

陷阱 真实例子 预防
类型保持 错误类型 验证