563 5 Tamper Resistant Software Architectures

Views:
 
Category: Entertainment
     
 

Presentation Description

No description available.

Comments

Presentation Transcript

563.5 Tamper-Resistant Software Architectures: 

563.5 Tamper-Resistant Software Architectures Presented by: Carl A. Gunter University of Illinois Spring 2006

Tamper-Resistant Software: 

Tamper-Resistant Software It is common for software vendors to place their software into the hands of not-fully-trusted parties. Such vendors seek to limit the ways in which this software can be used while maintaining valuable flexibility. Case study: OpEm Project at Penn.

Embedded Computers: 

Embedded Computers Embedded computer systems are ones installed in host devices such as: Appliances Cell phones Medical devices Vehicles They typically have one or more constraints on: Form (viz. size, shape, and weight) Power Location (mobility) This results in limits on memory, computation, and connectivity.

Open APIs: 

Open APIs Servers and desktop computers typically offer the ability to add software from independent vendors through an open Application Programming Interface (API). Some small mobile devices offer this as well: Typical for PDAs Coming for cell phones Devices with open APIs have advantages: Greater flexibility Independent vendor support

Vertical Integration: 

Applications Internal API Hardware Vendor 1 Vendor 2 Vendor 3 Vertical Integration

Toward Horizontal Integration: 

Hardware Applications Toward Horizontal Integration Open API

Open APIs for Embedded Computers: 

Open APIs for Embedded Computers Most embedded computers do not offer open APIs. Such devices often have significant constraints on safety (vehicles) and/or security (key tokens). Issues relate to Flexibility (how much customization is useful?) Portability (will it work on all devices?) Extensibility (can it add new functions?) Predictability (are there bad interactions?) Deliverability (how is software updated?)

Delivery Architectures: 

Delivery Architectures

Programmable Microwave Ovens: 

Programmable Microwave Ovens Microwave ovens are very widely used and they are crudely programmable: Hardware: microwave oven vendors Software: frozen food manufacturers There are key programming limitations. User bottleneck Standardization Complexity (e.g. multi-modal ovens) “Network dependencies” Goodloe McDougall Gunter Alur 02

Sample Recipe: 

Sample Recipe 1. Make 1 inch slit in plastic 2. 50% power for 5 minutes 3. Remove plastic overwrap 4. Rotate tray 1/2 turn 5. 100% for 1:45 English language recipe taken from food package

M/W Architectural Options: 

M/W Architectural Options Access recipe over the Internet (Sharp) Put the program on the package as a linear barcode (TrueCook+, compare VCR+) Use a linear barcode to index a recipe in a DB Use a Java program encoded in an “active” 2D barcode (OpEm) Kit Yam, 1999

Recipe as Java Program: 

Recipe as Java Program Enhanced recipe with extra functionality Handles cooling Adapts to oven capabilities while (inMicro.getCookTime() < 300) { try { inMicro.cook(50, 300 - inMicro.getCookTime(), true); } catch (PauseException pe) { try { inMicro.decrementCookTime(1); } catch (StartException se) { //loop again } } } Fragment of Java program

Java Program as Barcode : 

Java Program as Barcode Xerox DataGlyph: 1KB per Sq inch “I expect you can cook most things in one kilobyte.” Roger Needham

Active Barcode Recipes: Lessons: 

Active Barcode Recipes: Lessons Delivery mechanism is a primary constraint. Compression works even on small programs. Small programs offer a better opportunity for analysis. Existing formal approaches do not match the problem exactly: would like to do more analysis for a simpler problem. Example: show, statically, that a given recipe uses no more than n minutes of power and no less than m minutes.

Advantages of Remote Control: 

Advantages of Remote Control Embedded computers have many constraints. Why not shift intelligence to capable computers and control devices over a network? Example: smart cards vs. magnetic stripes. Vending machines Coffee shops

Payment Cards: 

Payment Cards Payment cards are a ubiquitous means for making purchases. There are several kinds: Credit cards Charge cards Debit cards They are issued by parties such as banks and stores. Approvals and payments are managed by card networks such as Visa, MasterCard, and American Express.

How Payment Cards Work: 

How Payment Cards Work (Open Loop Systems)

Payment Cards on the Internet: 

Payment Cards on the Internet

Fraud: 

Fraud Fraud is a major problem for Internet-based payment card transactions. The Secure Electronic Transactions (SET) protocol was designed by MasterCard and Visa in 1996 to address this. Now controlled by SETCo. Efforts were made to protect SET secrets from untrusted hosts by using a smart card Chip Electronic Commerce (CEC) Spec, EMV Chip SET (C-Set), Cybercard vWALLET, e-COMM pilot, Gemplus, Visa International, France Telecom, BNP, Societe Generale, Credit Lyonnais Doch, SET for the JavaCard (more later), M Lyubich Other fraud prevention mechanisms: Verified by Visa

Secure Transaction Problem: 

Secure Transaction Problem Bob Place Order Request Payment Make Payment Deliver Goods Secure Channels

Programmable Payment Cards (PPCs): 

Programmable Payment Cards (PPCs) Cards are commonly issued by banks to enterprises for use by enterprise employees. (“Corporate Cards”.) The bank/payment gateway enforce limited policies such as payment limits. Enterprises often want customized policies that banks do not wish to enforce. Can such policies be enforced by placing them as programs on the payment cards? Related work: card and financial management integration (eg. AMS). Gunter 03

Applications and Challenges for PPCs: 

Applications and Challenges for PPCs Applications Families GSM phones Raises many questions about architectures for embedded control. Can the card programming be made extensible? Which code goes where? Does the card have enough computing capacity to enforce policy? Does the card have enough information to enforce policy? Is there a feasible trust model?

Technologies for PPCs: 

Technologies for PPCs Smart cards Java Cards GlobalPlatform On-card verification of Java byte code SET on Java cards

Smart Cards: 

Smart Cards Smart cards (integrated circuit cards) were invented in late 1960’s. Widely used for personal identification, payment, communication, physical access. Microprocessor contact cards communicate and receive power through a Card Acceptance Device (CAD) attached to a host. Three kinds of memory Read Only Memory (ROM), ~64KB Electrical Erasable Programmable Read-Only Memory (EEPROM), ~16-64KB Random Access Memory (RAM), ~1-2KB

Java Cards: 

Java Cards API for using Java to program smart cards was introduced by Slumberger, Austin TX in 1996. Standard supported now by Sun JavaCard API Java Card Runtime Environment (JCRE) Java Card Virtual Machine (JCVM) Implemented by many card vendors. Other programmable cards: MultOS, Smart Card for Windows.

GlobalPlatform: 

GlobalPlatform Difficult to verify byte code on cards. Multi-application cards may integrate applications that do not trust each other. Open Platform was introduced by Visa in 1990 to provide a foundation for secure multi-application cards. GlobalPlatform industry consortium now maintains the standard. This is coming to be implemented by several card vendors, especially for the Java Card. This will provide an open API for smart cards.

GlobalPlatform Architecture: 

GlobalPlatform Architecture

Global Platform Process: 

Global Platform Process

Byte Code Verification on Java Cards: 

Byte Code Verification on Java Cards Sun Java byte code verifier takes uses too much memory to run on a smart card. Defensive virtual machine that checks types dynamically is expensive. Can perhaps use “verification evidence” to ease card verification burden. Technique used in Sun CLDC for mobiles: Pre-verifier produces type maps. These are used to aid verification on the mobile device.

Process for Safe Bytecode on Card: 

Process for Safe Bytecode on Card CAP = Converted APlet Leroy 2002

With On-Card Verification: 

With On-Card Verification

Payment Protocols for Java Cards: 

Payment Protocols for Java Cards SET is a complex protocol. Implementing it on Java Cards is a challenge. Work of Mykhailo Lyubich shows how to do this for protection of confidentiality of keys and card secrets. Target property: after a card is removed from a corrupted terminal, the terminal cannot perform further unauthorized transactions. This also “protects” the card from its user.

Challenges for SET on Java Cards: 

Challenges for SET on Java Cards Checking certificates is a challenge. Certificate chains are large and can be of variable size. Certificates have expiration dates, but cards may not have clocks. Sample problem PReq message includes information for P such as the PANData encrypted under the key of P If the terminal is trusted to check the certificate of P it could substitute its own key for this encryption. Possible to address certificate and time problems and determine operations that must be on card based on multi-level security model. Doch prototype software implements SET with confidentiality protection.

PPC Design and Implementation: 

PPC Design and Implementation Many of the necessary technologies are in place Smart cards (IBM JCOP21id, Oberthur CosmopolIC 2.1v4, 32KB) Java Card 2.1.1 GlobalPlatform 2.0.1 Doch implements SET on the Java Card for confidentiality Need to design and implement SET for authorization on the GlobalPlatform An architecture for policies and their integration Someday: on-card verification

Refinement Architecture: 

Refinement Architecture Refinement is a well-understood central concept in formal modeling of computer systems. Specify a family of sensitive events Show that an implementation limits the collection of sensitive events Non-sensitive events may be added Filtering is a simple way to ensure refinement Example: packet network filtering firewall

Conjunctive Filter Model: 

Conjunctive Filter Model We implement PPCs as a conjunction of PReq filters. The filters are written in the Java Card language and implement predicates over OrderDesc, PurchAmt. The extensible framework is installed by the primary provider. Policies may be installed by one or more secondary providers. Users may select their own hosts and host software.

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Create card with security domain(s). Card Host

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Program transaction applet, get card. TApp Host

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Certify applet code, create installation instructions. TApp Host

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Obtain certified CAP file and authorized load and install instructions. Host TApp

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Install TApp. Host TApp

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Create, obtain certification for, and install approval applet. Host TApp AApp

Card Programming Process: 

Card Programming Process Card Issuer Primary Provider User Secondary Provider Certification Server Obtain card and user-trusted host code. Use card in user-trusted host. Host Host Code

PPC Installation Messages: 

PPC Installation Messages TApp AApp Host Card Manager Load and Install CAP Install Select Request AID Object AID Object OK Register OK OK

Trust Relations: 

Trust Relations Merchant User Secondary Provider Payment Gateway Host Host Code

Card Use Process: 

Card Use Process Merchant User Secondary Provider Payment Gateway Host Host Code Select Purchase Item Obtain Approvals Complete SET Transaction

PPC Purchase Messages: 

PPC Purchase Messages AApp 2 AApp 1 Host TApp Ok PReq Ok OrderDesc, PurchAmt OrderDesc, PurchAmt OrderDesc, PurchAmt

PPC Prototype Implementation: 

PPC Prototype Implementation Doch on IBM JCOP with GlobalPlatform extensions Refinement architecture implemented using simple conjunction of filters Compete version for Oberthur cards Needed: an approach to getting timely off-card data

Current and Future Work: 

Current and Future Work Policies for GSM Policy integration: Polaris Code splitting: Protocols and Implementation of Smart Card Enabled Security (PISCES)

Policies for GSM: 

Policies for GSM Program the SIM in a cell phone so that it restricts calls Limit calls that might exceed base service charges. Nanny can only call the parents. Architecture in current protocols trusts the Mobile Environment (ME). Design a protocol to take the ME out of the trusted base. Weiner Gunter 04

Polaris: 

Polaris Advance beyond the conjunctive filter model Votes based on defeasible logic with state represented in an extended finite state machine called a policy automaton GUI for policy design Analysis engine for determining consistency of policies McDougall Alur Gunter 04 McDougall 04

Polaris: 

Polaris Advance beyond the conjunctive filter model Votes based on defeasible logic with state represented in an extended finite state machine called a policy automaton GUI for policy design Analysis engine for determining consistency of policies Literals: p, q, :p, :q Strict Rules: penguin ! : fly Defeasible Rules: bird ) fly Defeater Rules: injured à : fly

Example PolicyAutomaton: 

Example PolicyAutomaton “At most 2 purchases over $100” m1 m2 m3 yes & t.p>100 yes & t.p>100 if true then {}) yes if true then {})yes if t.p >100 then {} ) : yes d: R: M:

Polaris Architecture: 

platform Polaris Architecture Front end Analysis engine Code generator automata, properties results, counter-examples automata Java Card compiler (Oberthur) Java applets

Polaris GUI: 

Polaris GUI

Analysis: 

Analysis Reachability to find all states Conflict Given a state (q1,…,qk), check all combinations of votes to see if f(…)=>. Evaluating f(…) is fast (can be linear). Redundancy of P1: if for all reachable states, 8 t yielding votes d1,…,dk f(d2,…,dk) = f(d1,d2,…,dk) Maher Rock Angoniou Billington Miller 01 provides decision procedure

Runtime Architecture: 

Java Card Runtime Architecture Manager Applet P1 P2 P3 Policy Applets trans. info votes update Card terminal

On-Card Defeasible Logic: 

On-Card Defeasible Logic Design Votes in EEPROM, proof status in RAM Memory required: ~size of theory RAM required: ~number of literals Software Basic manager applet (includes defeasible logic engine): 3300 bytes Space required for applet: 600-700 bytes Oberthur CosmopolIC with 32K EEPROM can hold ~30 policies. Performance A transaction can be processed in 2-3 seconds with Oberthur CosmopolIC

PISCES: 

PISCES New project: Protocols and Implementation for Smart Card Enabled Software Focus on two technologies Information flow Model-based design

Conclusions: 

Conclusions Diverse challenges for tamper-resistant software architectures. Connection with open embedded devices. Challenges in resource management if tamper-resistant hardware is used. Suitable application architectures are critical. Analysis is harder in some ways, but easier in others.

authorStream Live Help