563 5 Tamper Resistant Software Architectures

Information about 563 5 Tamper Resistant Software Architectures

Published on December 4, 2007

Author: Kliment

Source: authorstream.com

Content

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.

Related presentations


Other presentations created by Kliment

Julius Caesar
01. 11. 2007
0 views

Julius Caesar

Because of Winn Dixie Irivarren
24. 02. 2008
0 views

Because of Winn Dixie Irivarren

costs
04. 10. 2007
0 views

costs

Johnson ANS
26. 10. 2007
0 views

Johnson ANS

Feroci LNF7may07
29. 10. 2007
0 views

Feroci LNF7may07

cultural dimensions
28. 11. 2007
0 views

cultural dimensions

savanna st
29. 11. 2007
0 views

savanna st

A C 16 US CHAPTER
31. 10. 2007
0 views

A C 16 US CHAPTER

00 19 pp7
05. 11. 2007
0 views

00 19 pp7

Ninja
20. 11. 2007
0 views

Ninja

Eng DeutscheConference 2004
23. 11. 2007
0 views

Eng DeutscheConference 2004

obesidade infantil
28. 12. 2007
0 views

obesidade infantil

Hydro Forming
02. 01. 2008
0 views

Hydro Forming

mental health powerpoint
04. 01. 2008
0 views

mental health powerpoint

gogel
04. 01. 2008
0 views

gogel

Final Ghana presentation sophie
04. 01. 2008
0 views

Final Ghana presentation sophie

Civil Security
07. 01. 2008
0 views

Civil Security

Displacement GK 4th
06. 11. 2007
0 views

Displacement GK 4th

23 7 2007enghlish
24. 10. 2007
0 views

23 7 2007enghlish

gas
30. 10. 2007
0 views

gas

heckls
15. 11. 2007
0 views

heckls

SmokeFree Workplace Policies
07. 12. 2007
0 views

SmokeFree Workplace Policies

annualresults0304
20. 02. 2008
0 views

annualresults0304

Chapter 15 Section 4
27. 02. 2008
0 views

Chapter 15 Section 4

Hartz2
16. 11. 2007
0 views

Hartz2

vedbhawan
13. 12. 2007
0 views

vedbhawan

nemo 4
03. 01. 2008
0 views

nemo 4

Advice for US Companies in China
15. 11. 2007
0 views

Advice for US Companies in China

LondonPreDepartureIn tern2008
14. 03. 2008
0 views

LondonPreDepartureIn tern2008

AnneMurphy
27. 03. 2008
0 views

AnneMurphy

Lt4 OpportunitySearch
30. 03. 2008
0 views

Lt4 OpportunitySearch

canCanadaVendorRequi rements
06. 11. 2007
0 views

canCanadaVendorRequi rements

MZ Investor Presentation Nov 07
13. 04. 2008
0 views

MZ Investor Presentation Nov 07

catalog bbc
22. 11. 2007
0 views

catalog bbc

2003 10 28 wendy
01. 12. 2007
0 views

2003 10 28 wendy

strategia
21. 11. 2007
0 views

strategia

alternative therapies
05. 12. 2007
0 views

alternative therapies

Repro 2007 Behague
02. 01. 2008
0 views

Repro 2007 Behague

celtico
06. 11. 2007
0 views

celtico

narrows2s
08. 11. 2007
0 views

narrows2s

MASINT5 Industry Brief Approved
30. 12. 2007
0 views

MASINT5 Industry Brief Approved

VGLAscoringguidelines
24. 12. 2007
0 views

VGLAscoringguidelines

O is for Oklahoma
03. 10. 2007
0 views

O is for Oklahoma

uiuc indri
16. 11. 2007
0 views

uiuc indri

Lecture3 History Fall 2007
05. 01. 2008
0 views

Lecture3 History Fall 2007

lis510n06a 02
30. 10. 2007
0 views

lis510n06a 02

PR Strauss
01. 11. 2007
0 views

PR Strauss