USL Security Features¶

entity User {
  email: String                      // Plain text
  password: Secret<Hashed>           // Bcrypt/Argon2 hash
  ssn: Secret<Encrypted>             // AES-256-GCM encryption
  credit_card: Secret<Tokenized>     // Token replacement
}

entity User {
  password: Secret<Hashed>
}

behavior GetPassword(user: User) -> String {  // ❌ E401 Error
  return user.password  // Cannot expose secret
}

behavior VerifyPassword(user: User, input: String) -> Bool {
  return verify(input, user.password)  // ✅ Comparison OK
}

behavior LeakSecret(user: User) {
  let plain: String = user.password as String  // ❌ E402 Error
}

behavior CheckPassword(user: User, input: String) -> Bool {
  return user.password == input  // ❌ E403 Error
}

escape VerifyPassword(plain: String, hash: Secret<Hashed>) -> Bool 
  adapter "bcrypt_verify"

behavior CheckPassword(user: User, input: String) -> Bool {
  return VerifyPassword(input, user.password)  // ✅ OK
}

behavior UpdatePassword(user: User, password: Secret<Hashed>) {
  if (password.length < 8) {
    throw "Password too short: {password}"  // ❌ E404 Error
  }
}

behavior UpdatePassword(user: User, password: Secret<Hashed>) {
  if (password.length < 8) {
    throw "Password too short"  // ✅ OK
  }
}

policy CanReadUser(actor: User, target: User) {
  actor.id == target.id ||       // Users can read their own data
  actor.role == "admin" ||       // Admins can read any user
  actor.friends.contains(target) // Friends can read each other
}

behavior GetUser(actor: User, id: String) -> User {
  authorize CanReadUser(actor, User.findById(id))
  expose Read[User]
}

behavior UpdateUser(actor: User, id: String, data: UserData) {
  let user = User.findById(id)
  authorize CanUpdateUser(actor, user)

  if (data.email.isDefined) {
    user.email = data.email.get  // ✅ Authorized
  }

  if (data.password.isDefined) {
    user.password = data.password.get  // ✅ Authorized
  }

  user.save()  // ✅ All paths authorized
}

policy CanEditPost(user: User, post: Post) {
  user.id == post.authorId &&
  post.createdAt.plusHours(24) > now()  // Can edit within 24 hours
}

policy CanAccessResource(user: User, resource: Resource) {
  user.role == "superadmin" ||
  (user.role == "admin" && resource.org == user.org) ||
  (user.role == "member" && resource.owner == user.id)
}

policy CanTransferMoney(user: User, amount: Money) {
  user.verified == true &&
  user.mfaEnabled == true &&
  user.recentMfaCheck.plusMinutes(5) > now() &&
  amount < user.dailyLimit
}

escape ValidateEmail(email: String) -> Bool 
  adapter "email_validator"

escape SendNotification(user: User, message: String) -> Void
  adapter "notification_service"

┌─────────────┐
│  API Layer  │  (HTTP, GraphQL, gRPC)
└──────┬──────┘
       │
┌──────▼──────┐
│Service Layer│  (Orchestration, composition)
└──────┬──────┘
       │
┌──────▼──────┐
│Domain Layer │  (Business logic, pure functions)
└──────┬──────┘
       │
┌──────▼──────┐
│Query Layer  │  (Database reads, caching)
└─────────────┘

domain behavior CalculateTotal(items: List<Item>) -> Money {
  let result = Database.query("SELECT SUM(price) FROM items")  // ❌ E601
  return result
}

query GetItemsTotal() -> Money {
  return Database.query("SELECT SUM(price) FROM items")  // ✅ OK
}

domain behavior CalculateTotal(items: List<Item>) -> Money {
  return items.sum(item => item.price)  // ✅ Pure function
}

service behavior CreateOrder(user: User, items: List<Item>) {
  Database.insert("INSERT INTO orders ...")  // ❌ E602
}

query CreateOrderRecord(order: Order) -> Order {
  return Database.insert(order)  // ✅ OK
}

service behavior CreateOrder(user: User, items: List<Item>) {
  let order = Order.new(user, items)
  CreateOrderRecord(order)  // ✅ OK
}

query UpdateUserEmail(userId: String, email: String) {
  Database.update("UPDATE users SET email = $1 WHERE id = $2", [email, userId])  // ❌ E651
}

service behavior UpdateUserEmail(userId: String, email: String) {
  authorize CanUpdateUser(currentUser(), User.findById(userId))
  Database.update("UPDATE users SET email = $1 WHERE id = $2", [email, userId])  // ✅ OK
}

query FindUserByEmail(email: String) -> User? {
  return Database.query("SELECT * FROM users WHERE email = $1", [email])
}

behavior PureCalculation(x: Int) -> Int {
  return x * 2  // No effects
}

behavior ReadDatabase(id: String) -> User effect Read {
  return Database.query(...)  // Read effect
}

behavior WriteDatabase(user: User) effect Write {
  Database.insert(user)  // Write effect
}

behavior SendEmail(user: User) effect IO {
  EmailService.send(...)  // I/O effect
}

behavior CreateAndNotifyUser(data: UserData) effect Write, IO {
  let user = CreateUser(data)      // Write effect
  SendWelcomeEmail(user)           // IO effect
  return user
}

behavior UpdateUser(actor: User, target: User, data: UserData) {
  authorize CanUpdateUser(actor, target)

  if (data.email.isDefined) {
    target.email = data.email.get
  }

  if (data.password.isDefined) {
    target.password = data.password.get
  }
}

// Proof: All paths (4 total) have authorization
// Path 1: email=true, password=true → authorized
// Path 2: email=true, password=false → authorized
// Path 3: email=false, password=true → authorized
// Path 4: email=false, password=false → authorized

entity BankAccount {
  balance: Money

  invariant BalanceNonNegative {
    balance >= 0
  }
}

behavior Withdraw(account: BankAccount, amount: Money) {
  if (account.balance >= amount) {
    account.balance = account.balance - amount
  } else {
    throw "Insufficient funds"
  }
}

// Proof: Invariant holds after withdraw
// If (balance >= amount): new_balance = balance - amount >= 0 ✓
// Else: throws error (balance unchanged) ✓

capability FileRead(path: String)
capability FileWrite(path: String)

behavior ReadFile(path: String) -> String 
  requires FileRead(path) {
  return FileSystem.read(path)
}

import AuthModule from "github.com/acme/auth" 
  trust "verified"

import BetaFeature from "./experimental/feature"
  trust "internal"

export entity User {
  expose [id, email]  // Only these fields exported
  hide [password, ssn]  // Never exported
}