Towards a Theory of Accountability and Audit
Towards a Theory of Accountability and Audit
Radha Jagadeesan1’*, Alan Jeffrey2, Corin Pitcher1, and James Riely1’*
1 School of Computing, DePaul University
2 Bell Labs, Alcatel-Lucent
Abstract. Accountability mechanisms, which rely on after-the-fact verification, are an attractive means to enforce authorization policies. In this paper, we describe an operational model,.' accountability-based distributed syslcins.Wc describe analyses which support both the desist ofaccoyntabrlrtysysturnsandthu vahdatron of audrtors for fimtary accountably systerna. Our shade daovides formal foundations to explore the tradeoffs underlying the design of accountability systems including: the power of the auditor, the efficiency of the audit protocol, the requirements placed on the agents, and the requirements placed on the communication infrastructure.
-
1 Introduction
The context of our paper is a^aif^^2^a^ciif^rndtstt^^f)i^tf^ot systums. Thu attackous tliafwe consider are untrustworthy peincipaisrunaing urbitrueyprogcams etn the netwoek. /tt-tackers may not respect the do-icle-od u syctem.fOT ea^^^r^le,at^£^ce^^^a mau create authorization objects withouiacdualty hev.n9 rhe uights to create them, aiming to subvert the global authorization policy. Traditionally, authorization policies are enforced by controls trnposod bcOresgioedresdurces are accessed.......
Recently, there has been goeetrnteoert in accountability mechanisms that rely on after-the-fact verification (Weitzner et al. 2007). In this approach, audit logs record vital systems informatiooandou eu.itor useb these togitoi-deatify dieiionuat jmiiuipals and to assign blame wfar therchaifeari a vfolaeibn ofocearrilyqfifocyThelear ofbciap “caught” helps to achieveeacuriey fy deforrciico. irifheapuif octrepi-ionel law enforcement and organizational recucity. Aeuounialfomqil ..res acrfocalrofo m thcdevefopmout of trust during human mteracifon tFriadmencn. Gredm 1 o98t- nuts^ccauntaloihty fo viewed both as a toolto tchieve ^ibdi^iud uec.Ll-ity i lpm^prdand04)acn us a flrst-class design goal of services in .iitfoial.ed dis-rlbuted-asiemt (YumprefaneinddChaae20adi.
While designing for pccodntabill-9 iscubfle in genera- gEaiksen 2002g, mechae.sms to instrument systems to euiuport aeeoueiabihty hcaebaee c^aforedm aesera. a^f)efi|'.e applications: determinate dislnlii.lt.ediy-l.rlns ( I LtehoOeti eU aL 2ea7|, actworketorb.a (Yumerefendi and Chaseco°7,. vbHdeLn0 T^ quahty ouecrviccein-ms (Augyraki ei al. 2007), internpt protopo-iAaapeecepOcL 200e-dbd poliddPnforcpmebton tharedtfou-umpnts (Etallp and W.niibiioiifoJnoa'.
In comparison to hpnuaz apprcauheesuch asacccrs-conical1 hawevev.lieaeuotini-ability approach to sepi.ll■iiyiacki peneral foundatioua for modula enilpr)^rlnpd9-.g.
_
* Supported by NSF Cerear 03475a2.
M. Backes and P. Ning ^ds.l:PSOP^^ 2(^Cf^yOC57tnnp.l5^-raC|20C9. © Springer-Verlag Berlin Heidelberg 2009
Citing a small sample of references, access control has (a) operational models in the form of automata (Schneider 2000), with associated algebraic models based on regular expressions (Abadi et al. 2005); (b) logic-based declarative approaches in a fragment of many-sorted first-order predicate logic (Halpern and Weissman 2003; Li and Mitchell 2003); and (c) static analysis to validate the access-control properties of interfaces, e.g types for authorization (Fonrnet et al. 2005; Cirillo et ah 2008g
In this paper we make two contributions toward bringing such formal foundations to the study of accountability. First, we describe an operational model of accountability based systems. Honest and dishonest j^ri^r^i^ipif s aredescribedasagents in adistributed system where the commmuaattoe monel gunaoteespoirt-totpoint istegrity dridaul.hori-ticity. Auditors and othestrusied agendo (such aoirusrcd tlhrilparuesstdealdo mndelen internally as agents. Boheviues a0 allagericaredosgrideeds procedtes in a procurs alee-bra with discrete ti^na|ipurhen^rgk‘^ncnUldpityis e^eurc(^lln\'f()^^in^auttilse^^eeavilr■ to be completely determmvdby d^^mp^^isgnt hear breedves.
Second, we describe aiialysesiosupitosuhe dee^nof ercountabihty sysiemsand pm validation of auditorafor finitaey tgsrema (thove with frnitety many psirieipalsrsnl^li^le finite state processes whh fauCcty monnmetsogo He^). We compfin doiiusa t^teum to (turn-based) games; and utp adernal.nlo(.ompl.rai to^cio spnctfy asebsnponiien ef interest. This permitsus to gdaptexintmg madeLcIiecking algorg.p^ns for veoiflcaiien.
Our results provide yie fovnctationa 11000^37 to ant^lnsa Sadkaafft in the dusi.e as mechanisms that prisere pccoontabfihy. Thg^aeelialtyaonfltotmgdes^nparameters include the e^iciencyo^heol.ldil..l.he omousit o0 toeing. anu the requiredsce as message signing, watermarkia^esirpcte^utt pketies. Doe^r phokapc placeeoastsaierson the auditor, the agents of the syni.a‘m;md ..hamfieihysng vommunmattop infrasttuctme.
The paper is organiead asfollews^amptipate our agprevcg miction 2. Seciioe g describes the model and peeiiou 4ddtcsibet sloe aaatysH framewoslwThe Liens muto lustrated usiag exam^as m Spsfiea g. Wr stewa'yrehil.edsdork m 5^<^^isoii (5. Id rtoi extended abstract, we elide aliprooSs.
2 Overview of Our Asss)ii()ach
la this section, we illusSita toemotibationgbe0mbtopdesign uS am a^emewerbusinn variaats of a motivating g^eae’iplromdlkn0 et st ^070
la Sectioa 5, we pralycaar ahstractdSPiM0oetoeexampla toas avnetth met^e forwarding amoagst i^tscest^one^ssh^ndti Ouo analdas fields a variety of auditors for the example, evea ia geaeral distributed settiags, aad shows that powerful mechaaisms, such as trusted third parties, are aot accessary for all audit protocols.
Example 1 (My Health). The MyHealth patieat portal at Vaaderbilt Uaiversity Hospital allows patients to asteiacSwito hedtocaru dkofeiciodnts thsenuh a web basmtsysSem. There are three possible kelentoar can 0c ascumgdbmpiiiripals: dekatopporessioaals (doctors aad aurses), 301^631^110^01^1601^080,^0 pasternse Tha pgssible messages include heatth quistting from ppiienis anmhdaithanswertSrom U(^ctoo^. We focus on the two privpay hogeies ie Barto cSaLa0007): (a) a i^^^ndt quesfipe tun oely be directed to a healto proeesrionmi an0 SOs sc healtoneswgc e0avta patters cenoeSy be directed to the same patient or to a healto professional. These policies permit health
professionals to forward health information amongst themselves. In the discussion below, we will consider the case where patient Charlie contacts the auditor because he has received a health answer from doctor Bob that was intended for a different patient. The motivation for such an audit is to aid in the detection and discovery of the source of the leak. □
We now describe ourmodel jniditsrelation to the following properties. The discussion is intended to establish intuitions, with formalities defered to later sections.
- Upper bound: Every aeantguilty ofadishonett action isblamed bythe auditor.
- Lower bound: EverydUdHdmedby die talitol is guilty.
- Overlap: At least red of ide agente tlam-P bndraddilor ts entity
- Liveness: Hie auditoa if alwaaa sacdastguiir blanauga noa-empte ongtei od oidafH.
- Blamelessness: Hoeust agents have a strategy to avoid being pronounced a possible offender by an auditor.
Agents. We model lhg egbartoa et priorapgic (Ogga a ltd dlshoaesil Mart^
in a distributed system. Auduoroandalsomodeladrs hageai udenm. We s.n processes to specify an upper bound on htg^amt bebsviosia an■uc■pin■o behavmg bon-estly in a run wbeimaer tbeircoi,mbemyn go die nnmsa a-sensf as honea poocess. A dishonest agent is unconslrained. Aranpy an al^ell;l™nlll.i. dishonesty it it a mots permitted trace for an honest agenn.
The communication model captures point-to-point communication over an underlying secure c()^n^nll^lic^()nmecha^nsm wh.ch provides integrity and authenticity guarantees, but providesnoaddittosal mechamsmf lor aontra^rdiaiina ar ead-to-end security. This model .a terUzyblnesiag yastportmechunismt sschitt ■pI.g.
Dishonest agents maycollanolrie albilnariry.Thtcmeagetnnl toe tudhor hao do achieve its objectives indgpnndsnl of ^lentisl eeolelagf onchoneyt a^nln Hanest ageats may also collaborate^ependinjg ugen tnnlnnaiflcniirn ofnnnesingenin.
Intern.! auditors Acton. ssihdended ts as nuaiinabie agento tor 018^^1X1;-tem without global knwledny. n^as, tony tee Ms^^ nd tsaitfactiottr tauoda «.. voice them, and their Ideatst-e tn onlptuiSsiennedPp tyames-nainMttoayrnaalv-.to contrast, the strategie-edopley aa toalseeost_n8eniscad ynte1tilallydedeildul>vlewicg traffic outlie network between olyeiagelltd.uhetnthrltahzat;yl1 otaudltytshmlitlhem. Auditors can only totoa-s niyhnne!l bei,avlprs uan-g toe ■n-mmatiMi aaadabhnan lit dividual runs of a system; they aaunalaedlt rtolriions raseeerllepropeotlns Oauneayd sets of traces for their specification (such as non-interference). Auditors cannot detect cartels of dishonest agents whoconduct dishroest exchan^r nmon^t themtnlvet.
Thus, our auditors samoot in geaK‘ral samsn^ltn/;/Tni^^oluim Tn sat th.- aostkler the leakage of patieua re-oMstoa dtshyeaeinou-heaam ^nfesttonrl by edishouelt health professional vlaouilOf1n-ndmnchhnismr wiflimut usrn. iheMyl toaltliwehou.e in Example 1. Such tetkaga ofreanifs yy d^nensa eeyutt aelely to ^-.ainost ygnntt will not be detected aS ch byanauchlei iartn framawn-hl
Mandatory logging ana aespunslaaneai.Er.enm t aase tout tha .n u 11a a fas lan-omg aware of dishonest bnlipvior anr mnaaies anaudih an torCen y ntmerlnsetmntss ffisra are statutory and enforcyaMa rapsnmg rethuntamnyty onillnlienhsi agetus. .
In Example 1, if toere ts tt. raqrnten^a^nt eormalntumma n-a praaoaimg imo-K doctor Bob can achieve absence of provable guilt by maintaining no records. Such reasoning motivates requirements on honest agents to maintain audit logs in several accountability systems. Furthermore, a guarantee that honest principals provide answers to audit queries is needed for the auditor to achieve Liveness.
These desiderata motivate the inclusion of time in our system specification formalism to enable systems to mandate promptness on honest agents. Thus, auditors can use tardiness as evidence ter dishonesty and assign Marne to sohit rnrdy agents. Outmodei uses discrete time, which is abstract and logical rather than quantitative.
Communication model. Hie msH.de of mn-repudialio.. iaonrbds.ccomtnnmcation model limits-the acteuusyoete aodrt pmcey. la fnorme. For oesmpte, inlhe, audii scenario of Example 1, the auditor commences by querying doctor Bob: if Bob disagrees that he sent tte - - tu gadem Chaolie, tlie i ..o srn, ndoes urn at Most one of Boh or Charlie is coteproanseni TO nlosencn oSnnn-tonudiaiionoteeenetfurthsa disambiguation. AlternateOn- Bob . ■■ to another pnneipal. ns lhetandar
of the patient benltb mnrsage. In lime asp lheadeltaoproeaese Keqa^eihoe Toe. Tits process either ends in one of two ways, (a) The auditor discovers two principals (perhaps one of whom is a|o°.hf)nrtessi(oapuvho di-agreeon messoges.enEb0 ooe and received by the other,satketehed es(Ttumlltiscals. ^^ca.lt ehspsmdpalsaredeemed guilty, (b) The auditot^.Ea-^vei^s acynle of iioii-heah.h aitSc‘ssim.iilSi eachdarnieglo have received the mess-go fremtao .re1^:^^^-^-- in (heeyde; hi t^^s case, Fre satire cycle of principals is deemed guhty. Etehher case, smanritsinchievotLrtap.
This situation maybe nneaiisfasiory to ao hoaest s^nt, smsehh soOpol-ibsefot en honest agent to achieve Mameteseneso. pn anWhion the audhoocaanot aduevesKonger properties for the auditst,rpch e-Lmuer oos^nd.mush pse^rties sequiry msae decided and secure logging opesosssd^s.
We do not limit attontiou io stenngmodels (ifnammuineaiioK—ouch aslhesenn-abling non-repudiation—tecause weakermodds asaoftoamoso o^ul^i--. foeexemple. in the IETF Session Vitiation Psatoanl Snrht,s ..ypmaOdPp'nny h exhale0 to handle large volume of oatii, Lius. h -s d^cuhnn sueyesafutiy mandate colnpt.yrl.(sno0p expensive signature bassdmoihods on aecheyinltto-potstdommuplsstlotl Imk.
As evidence for theflnxibihty o. ouemadeling, we ^1^^-^ that (u-e mode1 oynii.deed encode notaries as trussed ehhd parties. u-e^^ permis.s lisi.o addresa thetlr,,.tssl■comt munication guarallleesrcquiie-l toeiixwoSdycapieoe examples such as the MyHealth website of Example 1.
3 Formalizing the Model
Based on a notion of -^i^s^t^^^^, dolined bnlaw, we will define ^preoat-r0.eCl^l ton. a set sd of principals, a seO -p-of messages, and a sue dC si nrasasses, whicOdeflna ths honest behaviors of a^^nlwlv^tes,wo sOall gieu eeumplee-nnas,aodthan give dssTaUtn properties of auditorn iy^ue^so eyene.
Our formal model is earndoaCammunicating Sequential Processes (Brookes et al. 1984), I/O automata (Lynch 2003), and discrete timed process algebra (Hennessy and Regan 1995). Our prosesses zreinput-enabled, to prevent a (perhaps dishonest) agent from blocking the output of other agents. We use discrete time, and the timeouts that it erigeittlotr. So specify condhions onp^^we-t^s^hchii-e. Ourcommunit cation model provides integrim ano auihereiony gussantees buO provides no addiuontil mechanisms for non-repudiation or end-to-end security. We use processes as a safety specification of honest behavior: a principal is behaving honestly in a run whenever their contribution to the run is a trace of an honest process.
Actions. Fix a countable set sf of principals and a countable set .// of messages. Let a, b, c, d, h range over elements of sf; A, B, C, D, H over subsets of xf; and m over elements of
The set of actions dff over (X .X) is then generated by the grammar
W s,oSaei I B
X’ .. Cl(J
’ 1
whereii lr.m represents a message m sentfrom a to b, andu representsatimeout.
Relative to a set of principals A, aaac-ioa may be output, ibpuO, ieteonab chooaine or timeout. The action (a-bb:m) is ootput from A ifne A and b Bi, input to Atf e A and b e A, internal toAifoe m td b e A, and disjoint from A if a A and b A. The action B is timeout fro mA for eu yA.
We often describe actions from the point of view of a particular principal, using ? for inputs and ! for outputs. Thus, when giving the example of a process for a, we will write a b:m as a^b\m and b a:m as ba'lm.
, r c . f o
Processes. A process ovei |sV^^i is r eusdrupSeP = 0,S,ro, ■ wbereXA CsA is a subset of principaiXb) S in a teiof states, ranged over by s anh ( (cXo-t S is a distinguished start sto-e, Sd( -+ CSx# x s t p ao-ltS PasiiSon reletioniewhich labels are actions over |X f}. We call A the-rincipaIs afP, written tt(P).
Jr
We say that s allows t whenever theae oxirrsa Osuchtoarr-i t.Wn miso sooutre that no label in iudis-oSai free A oveayatete in A allows evasy tofut fouA o
enabling), every state lo S atlows atle ast c time rut or ouSput for A (timeout-enabling).
Whenever A and B are disjoint we define the composition of processes P = (A,S, r0,^i) and <2 = Am. ■." to bePHgv.(A LjB,S || T, roUt.^t wOera S || T -| r / r 5 and / to saa' ei'' deftn^ es foilows:
r
S -^>1 s' t ^tt'
II „ k—m We disjoint fromB ---e-yp is desjasnS from A
jlK-riK rnis-ull a
> -Apb yXj Ok ioiepsOoA and ortpot free B, ue m|tXe|ie ^p f^o'e e andeutnut teem A, or O sb
We write n(6X« for the composi0onef process-t Pt.
A trace, v, w, is a finite sequence of actions. Write e for the empty trace, and v.w for trace composition. Write s : s' to indicate that tlicre exists a sequence of transitiens from 5 to s' labeled by v. A trace has priecipals A whenever it contaies op acOioo disjoint from A. A run of a process P with start state so is a troca v spsh re aoe' fosaome b. Note that any run of a process with principals A must hava pri-tipaes A.
Write v (A for the projection of v onto octioss relating to A:
e[A = £ v.(b-^ cm^A^IA SOAe^e, c} = 0
v.BfA = v|A.<t v.ib-^c-.m} -i s'A.-s^01/ ifo W t.,r ^ 0
Note that for any P with principals A and Q with principals B, v is a run of P || Q whenever v has principals A UB, vfA is a run of P, and v\B is a run of Q. This is the usual trace semantics of parallel composition in CSP (Brookes et al. 1984).
Arenas. An arena (sd, comprises a countable set of principals, a countable set of messages, and a countable set of process over (X .X).
Given a principal set H and a process P, we say that H is donest inPifP = n(6/X and for all h e Pl there exists Pi e such that 7t(Pi) = {h}, that is, if every honest principal must be repreoentedby an honest process.
We note that honesty for psocessee ssdown-closed (if H D TS md H id honest in P then H is honest in P) and umon-clodhd(if d edssdH cehenettih P then so is HkPHf, so any process has a maximum honest set of principals.
Given a principal setp andh trace v, we say thadd is ftoaoduah wlionover l.licrc exists a process P whit rnn if moh that Hk doneat inP. Honesty fonloaaen is dewn-closed and union-closed; so my Ssate hor anmihuim Isnconi set of prmcipals.
Honesty is a globa^rojnarty of ttases, foot H fon eny trace a captoring all behavior of the system, we can determiee thefirinc^ehd who hovh behavedtonestly in that trace. The problem of audit is that, the ao^tOTHnot proyfoeow^ the tsacevtoit otily a losal fragment of v
Example Arenas. In the following examples, we write principal nameswsthout sub. |
scripts or superscripto (n,h, IS andweitosiates belongineto s jMindpat witH numeric subscripts and optionaiprimhs (Po, h5t h^wim the conveeiiot hat m)i a nihte of an honest process with prinuipaln 0a}, a^idas PiH tie otari otatedf tho prohoss,
Honesty and dishoneaiy ore psopeotief os hrincieolr with oesystn a Orahe, rateer than an intrinsic propttty esn prihcinol.NonetOoSers, we fins ii heipSsi at toe ^^<0 names in examples to indicate poincipals that are intended to be honest or dishonest. We use p, q, r for general ^dpaf h, g, f for principals with honest behaviors; and d, c, b for principals with dishonest behavters. We alno use x, a o her paromotere and e for auditors, as discussed bdow.
We elide transitioaaraqurredroleie fehrn^t mnaloling, assuming an lmplioe. (transit tion pi pi for any O:^^^} acsininaa |s thatee na^phc^0 giver.
Example 2. Consider oh arena with es = {p, qf ond oI = {Nad}, onddefioe ah honest process for each h e roaf<^ivoni^hrrle leftmoet ofocardbelaw.
h^yibad
The initial state po || qo shows that both p and q are honest in any trace containing only timeouts.
p is also honest ie ttieiaoces t'dabad (becauao tho aoHon ildisrointwith ni and q p:bad (because p is input enabled), as witnessed by the initial state po || q), where q(, is defined by the center process above, q is dishonestin these traces, since there is no process that is honest for q which allows them. Moreover, q is dishonest in any trace containing q q:bad or q p:bad. Symmetrically, s is honest in pp:bad and p q:bad, whereas p is dishonest in these traces.
Auditing in this arena is trivial, since the sender of a bad message is guaranteed to be dishonest. This example corresponds to the case in Example 1 when no principal is allowed to forward health answers to anyone except the patient in question.
There is a problem with initiating audit, however, in that honest agents have no mechanism for reporting dishonest behavior, for example p cannot report the receipt of the message : to M aud.tor. □
Next, we model the message forwarding capabilities of principals in Example 1.
Example 3. In the variant given by the rightmost processabove, honest processes are allowed to forward tge firsS bad mesgraehgat tgve roreive; SosveampSe, oeeoegingdis-honest behavior to an ayestor. If enaudhor keowsthvt a mestave p^qiPatOesPoen sent, then there musfPe s dishonest prtncipai,hut doesnos know who ss dsaPvvost-there are traces contsining p-+q:badin whivhp io honest, or q is honest, or both. Hie goal of the auditor should be to determine the agent that initiated the bad message. □
Auditors. An arena with audit is an arena with a distinguished honest principal a and a set of distinguished messagesbla msB hop evgsy BCv/, ineteatm0 slit blnmetet B. For simplicity, we treat llieblame adtion as ieternal l.ol.hsotidnor. and thos svcalsbi'evioie the action “a- ■a:blameP>" asOaa^l^.mnB”
We now consider bosiquanotions oscerraotgess e^^obd-os^.:-^^na of dione notioni, while appealing, haveserious tesMcal gnvblems, addn owe nse n ot evvstdes them further in this paper.
In these definitions, we will discuss a trace with dishonest principals D, defined to be sf \ H where H is thelargest hvniestset
Candidate 1 (Upperboensl), An arona with au(Oifpnvviacs poo pgp^i leogcl ov shs-honesty if, for any troeo cwVP dishcneciD B a coniadning a:blameB, we haveD C B.
Unfortunately, the onle usdi-ema-eble pS pi^oi^iCmi>peup^ert^(^uohon PishonesSy is one which blames allpotncipaiaw-aaoe capable of dishonesty, regardless of whether they acted dishonestly or net.
A C si are said toSe capable o/disheneoty resto erene wSienever there is a trace v internal to A (i.e., all messages from a e A are sent to some b e A) with dishonest A.
Proposition 4. In anePoeno where auditpsovides an upper bound ondtshonesiyann where AB a are capable of dishonesty, we have that any trace containing a:blameB must have ACB.
We do not consider ties ogtit^a of coiPectnoss further.
Candidate 2 (LowerboundI, A aoena wish Mdtt nnvides <m SvssPO w - g. honesty if for any trace v with dishonest D a containing a:blameB, we have BCD.
Unfortunately, auditots ssrs only canrbleofblaming riehonest trinctpsls whnnunfesseO their own dishonesty. Dishonest principals who do not confess will never be blamed.
In a trace v with dishonest D 9 d, we say that d confessed whenever, for any w such that v [{d, a} = aS sve havePiaSw hes dishvpest D'9 P,
Proposition 5. In any arena where audit provides a lower bound on dishonesty, and any trace containing a:blame B with deB,we have that d confessed.
Trust mechanisms (such as trusted third parties) are required to establish the nonrepudiation implied in the above proposition. We discuss these in Section 5.
Candidate 3 (Overlap). An arena with audit provides oaorlapwith dishonAJty£./or any trace v with dishonest D a containing a:blameB, we have BOD = 0 implies B — tb.
Overlap is a more general property than providing a finite lowerbound, sinceany lower bound {dx,.. .,d„} can be replaced bya series of singleton overlaps {d)},..., o e
We do, however, notoonoproblym wtth thssdefini{iov,whichis that elthoufh ieie up-closed, it is not intersection-closed, that is there may be v.a:bla me B.w and v.a:bla me C.w which overlap with diC^^i^^sty, but v.a:blame(B F t) uedoei eot.Tinis mayurise incaies of separation of duty (Frrnatelo at ni. UOOrUiiap and q murldtehoopsOycolluae tn u^uta some action, then an auditor might choose to blame either {p} or {q }, but not 0. We leave this problem for future work.
Candidate 4 (Liveneso)tAn arena with oodie is o-Oiveiffoo anyruo v.k.wsooh thato is honest, k is an input tote, andwsnneaioo nt item ofte me cctione.thereio anatsion a:blame B in w. An atenawioh aodie is ^ivewOon^e^eett Icn-lfvcfoe rove n.
As is common with ooereotoeso oriteria, vc vieoinomsh beOween safoty pryperttea .o liveness properties. Ie me caeo, livenees MeOo rhecleioo^es^By ord eerie} (ainoe np arena is n-live preciseiy wOoe ehy honest peonooses for a are n-live).
4 Analysis Using Turm-BasedGames
a t c .. . . e • a.,
This section describes the use of game-based methods to automate the analysis of the properties described hi theoriorooctioc. Wereoer bit reeder ne tAlweOai. en^S.wr background motivation loiddoOofed erlm1picSl
Definition 6. A turnobased oame ^eph oves ifplcyessp.ayoi ato pla^r oh A i±i • • • yp.yn,<H,n,if) where:
- (5^, A) is a directed graph witha total transition relatia-^ over r-a finite stateset AL paatiiipe or oo aied se (he «((«.....
" n 1S > s“ of ProPo0ihoesi ef e f -o e yoMe Uo pr0fasopmo erunat ecd> e^ □
An evolution proceeds; asfollowe. yt.alne in Ao oeeptayee-z stotre, where player i decides the successor state. A -ahi inhhe game eraph sn aMSe o(Sefiiliee sequovee of ovees. By totality, every finite path extends to a play, an infinite path of states.
Strategies. A (pure) strategy for a player is a recipe to extend a play, i.e., given a finite sequence of states, representinglhe hieis^ otihe ^ay a stealoepfos o player choone-a unique successor state So ..tesd the play.
Let menu be a set cailed mamoay thaleIlcopes hie mlorrnaliietabout dio Oistorpof the play. A player i sttategy can be described as a pair of functiens: a memory-update function gu: 2n‘ x menu menu to update the memory with the current state and a next-move function gM that yields a new player i move for every element of b x menu. A strategy must prescribe only available moves, i.e., for all s e for all m e mem, we have (5, gM(s,my) e S.
Let stand for the set of valid player i strategies under consideration. Strategies interact aa follows. Player i tollewsthe .' ■ ■• s if tn each player, move, she chooses the next state according to ij(M. Once a starting state s Z and strategies g e % of the players are fixed, it is clear that toe resulting outcome is a play of the game.
Compilation. We compile v Unite collection y Unite acKprocesms (with it ttaiee universe of messages) mtn a tnm-t.ashdgame.ohe (tattnlattott nees new prnpos,tt . . guilt for every p e sZ. If guilcp is satisfied by a state on a path, then p 1 s dishonest on t at pat
Logic. We use a fragmentof tie lopicATI.' tAlur et cl. 20d2). arte usablepeoposstions are restricted to the ones of inieoest.TPe pato tosmulas oeclede the neoiiiiedMity
As a result, Ute proneetieo ieeinseneitiveto ihneolea ttansisiops introduced by tic above compilation ot arenas mmturn-leaped garnet .
We refer to Alurassn. 2eO2) for poeeise semnnaha.TOie stem (0) and eoot tistaae gtven by the tollowmggrammar: eet is ey subselof p^2^
0 ::=true \gsUtp | cr | a:blame B | p q:rn M I 0V0 | ((A)) p y::=true |g bd | pV pip p p ti p
The formula b> p is.eueat aieste if frete exiet sl.rai.eg.esler fro e|ayeatm sei. . snih that no matter what strategy. fre ofrer players (in .hecempleme.tt o. Ai ceoesa,thp resulting play satisfiestPn pafrSotmula p.
We use existential and unreerstl quantiflcalioyoveeflnite sets effn‘aip pf flo.te n)e-junction and conjunctive; e.y., (eletittcc shorfrayffor (VPip. A.am, we ds.ine
- NonZeno = nOcr, to identify live traces with in finitely moey y astions.
- Alnit = 3p.m//i'p a:mi, to identifyttscee where fre auditor e lun eeen initialized by being sent somsmeeseye.
- Succ{B) = NonZeno exArnyni ^(woieme ^er e idenPfyNon-eeno laacoe wtmse fre auditor has been ceniactad annfrn sufrior leas a(slpnyd bl we to B.
and ________________________________________________
|
Oaerte^p |
((0MitccCBi = |
> (sa> n Bigtntp |
|
Lower bound |
iisns^tB) t |
ts i sio s |
Since the auditor is flxeV, frese ms LTL esoportias, t'lltle;)iey'lieo|BCcg.niin ATL*, frey have the strategy quantilierwifr the eiiiflv yet in capture universal quantification over all traces reflecting other player ehoices.The svundness ofthelogical encoding atave w.r.t. the trace based defl^ttices nt freaaotiar oeetionSoKewsSsom fre spueOesss nf fre
nas
Blamelessness of p for a fixed audit protocols true at a sltatit pply i f fr e as en t a has a strategy to ensure that p never ends up in the bitme set assigetP by ifr audster, independent of the given fixed auditor strategy and independent of any choice of strategies for the scheduler and theether p^ytes. Heesa||y.we define
r
|| BO!tmetonpnens | iip))(n(^B^p)O(ta:blameBi—fl
The model-checking problem for ATL*is 2EXPTIME in the size of the formula and PTIME-hard for bounded-size formulas (Alur et al. 2002). So, we have:
Proposition 7. The model-checking problem for Overlap, Lower bound and Blamelessness for an arena (sf, with a fixed audit protocol is solvable in EXPTIME in the size of the arena and 2EXPTIME in the formula size.
The formulas of interest are small. The bottleneck is the EXPTIMEdependciiue on arenas caused by the determinization of the honest processes in the compilation process.
5 Example Auditors
We present a series ofexamples in -w^l^i^rfi the audit or aims to detect. the origin of a special bad messagCiAttdf edd of this deeeien, werelate t^et discdpoion ^<e Exdmple 1.
Example 8. Consideraueliting the eeeainExample3. When theeuditom receivesa bad message, they knowthctthnre is edinhonnet prinpippl. ICep^'^c^ir sipcn fUm errein does not permit them to query principals for further information, they have no way to discover the guilty partes. So toe best they cando is blame everyone:
Ar ren ne
This auditor provides ISvemese and operivuwtth dithonesty,aineii trivial lysThis aeUttor does not provide lowerbonud. □
We now consider audif protocolswheryhouestprmcincfr re requirpdtn rnsuunU io requests for information from the auditor. From a principal h, the auditor will request the identity of the sender of a bad message to h. We analyze the variations that arise depending on whether: (a) honest principals may forward bad messages to principals other than the auditor; (b) honest principals are required to reportbad messages (all are allowed to report badmesttrep); Sep senders cecoft tewhom tSwy have lorwrded bud.
Example 9. Extend theerena of Exumple2 toaecommodate audit by setting = srf U {bad,audit, nobody}. TP□ac^i^i^^lt utosgrees re dpseribeduelpw,wyeee wedereribu the potentially inflnittJrigte teeptiltopsnrtepw uping itute variables x, y, xsrreydsg oveu szf. States hi, ai and ru re premeterized Vu printierl x, whish sent toa uad mes^^r^. State a3 is parameteri^^^bvieh priniipaHist xs, wPich ase Warned; we inc ii.n etab on for lists ([] for the empiytisi,:: fou dtvfipinx,© fprconcetenytion).
Honest principals may initiate an audit by reporting the receipt of a bad message to the auditor (the transition h a!bad at hi). The auditor responds to audit with a request for the sender of the bad message. If the auditor’s request (at a2) times out, or the response is nobody, then the principal initiating the audit is dishonest and is blamed. If the response x a?y is received, then the auditor blames {x,y} because it is unable to detect whether y imitated er fcrwaaded bad, er whether x is lying about receipt et bad from y. This auditor provides liveness and overlap with dishonesty. The algorithms of Section 4 verify this for the case when the number of principals is finite. □
We now analyze the consequeecec of tdlowing honestpaincipalsto forward badmes-sages to principals other iCan teeauditoc.
Example 10. Allowing honest principals to forward badmescages to all principals, as in Example 3, necessitates chagangtee auditor to nenk dr am ehe (edgfcctt samee of the bad message. To s^tse this, fint modfry -de neerr UromExumaie 9 by aealacimg Che h^a!bad self-loop o-Mxi with ea>n!bsd.
The auditor from Example 9 does not provide an overlap with dishonesty for this new arena, because a trace oktheform da-C!bat, hagJba-i g->e!bad,. ..wbuldresuli in g and perhaps h beinebaumed incorarcdy adieiafocwffdind behavior is honest) when only d has been dishonest (initially sending bad).
To identify an originator of aba d measage S-^^^ii may hasbvera!).!.fe aehit osbelow follows a chain of forwardess until y rcce.ves: (cSferespocae (aLimeoutd.t'h) tea am swer nobody; (c) theanewer a^r (ad l finds c uycle os forwfrrtere. The neditoriheii blames: (a) the principah toti dial not reepond to aa cudit request (it is dishonest to ignore the auditor); (b) theprineipe- pateem aerpaeUad wh^ nobode and,ia teeae a oae, the principal q that clamlet;i>fon^vaebad ba^eqcaitees q is lyhte nboul. rteeivin! a forwarded bad or p is unable to.dendfyr princmal thatfo)waufe° bad toteem);(cb^e principal that 0^11116^ torwmxlet;ead.eeat.prinaipelif b'ingbeeauee the auditor does not send bad); (d) all prinrqaala m tee eona efthemH iyiac cbouStee souaea).
States ai, a2 and a? aaepabmeteaizedby)halirtof fnsuectedpritlcicels.
ag^ud^c0cs
—, atblame {x::ys} if xs ysS xSzs
ao k---------aeem---------
at(y::x::xs)
~i Xam'y
(T
x^a?nobody if xs=[]
x^a?nobody if xs=y::ys
This auditor provides liveness and overlap whh drshonesty. The algoriflims oif Section 4 verify this for the case when the number of principals is finite. □
It is important in the above example that the arena requires hondst principals to record the initial sender of bad rather than the most recent sender to make iheaudiion overlap with dishonesty. (If instead the rnrrst pecpnt sender of bnd was reported to the auditor, and we saw a trace ending wite a cycle off the form d^hlbad, lwg!badg g -h-bad. h a! ba d,..., then the auditor would find and blame the cycle h to g to h. Neither g nor h are dishonest, so the auditor above would not overlap with dishonesty for the modified arena.)
In both Example 9 and Example 10, an honest agent is unable to achieve Blamelessness. We address this issue next by encoding the use of notaries as trusted third parties to permit honest agents to establish blamelessness.
Notaries. The presence of notaries provides a non-repudiation function and disables the ability of a dishonest principal d to get an honest principal h blamed (by simply claiming that h sent bart to C(. Hie noCatfprincifais tw assumed to be Woncst. Cor this reason, we refer io rhe notary principals as Trusted Third Parties (TTPs). Here we consider a single non-audibor prindpal for ihr sake of oimpliritcibut ilio^ot esriattai that there be only oneTTP.
We assume a colleotionpS mi^agest'Et g tOat sass uninterpreted through the TTP. We define to include the bad message with different provenance chains indicating the path of the bad messago.Wilh Alioeal.wei.heri drflno toe metsrgei oftheaasnsby: PC a
,<=(^|x^) (Mesaasos to und fromTTPS
U (.e/ x -Af A) (Mossa^oiuery b.rutotor to TTP|
U {yed,ro. rnknown} (Re^nnoe toauditor)
We use f to range over forovtooe^ipo fedinls tsi too fprmfx, y, e) indicaiingtOatthe TTP forwarded g from x to O- We use Ftorrnge ocorsets pO lonnt'ardiiigreofods.
The TTP interactswithpsincepals byfpnwoSicg mestngas onthetobhOaif. A principal x sends a forwarding request of the form (y, g) to the TTP (indicating the target). Subsequently, the TTP forwards toe message (x, g) (indicatino tonoou(certoo, ann adds the forwarding record (x, y, g) to ite store. Tire TTP also respond to quelto‘flsom the auditor that ask whether f = (x,o, g) has been forwrnded io toe pant st noo only respond honestly with yes (resp. no) if its store contains toe forwarding record f (resp. does not contain the fotwarding record ft.
The TTP state ttp(^a^;^,^s) )s(Aramoterioed |oo thioere-s of torwartorigrecotdr. The set Fx stores which messnges hovebean foawrrddto Tire pct^ mrintainr tot forwarding requests receded lrotno. yo‘t.aftod i.loorl.Thosei. P( piantt.dins the auditor requests received but noSoetorten u^n.TOe TTPmtiy only dmerml. when tonrcarr no actions to complete, Ln.^t ft 0. rne trisrf actions mot yti compete. sre present to ensure that the TTP d mpui onceiee. Tae tehavfor of the TTC is s^rtood as:
Provenance. We add provenance information to the messages.In this contexi, provenance is a sequence (possibly empty) of principa) names indicating the path of a forwarded message. An empty provenance sequence indicates that the message was not
forwarded, i.e., in x^y!(bad,e), x is confessing to sending bad directly. In contrast, a non-empty provenance sequence of the form (z::xs) indicates that the message was forwarded with z being the most recent forwarder, i.e., in x y! (bad, (z:: xs)), x is claiming that they received the forwarded message from z as z-x? (ba d, xs). We now demand that honest communication between principals occurs via the TTP (operating without knowledge of the struotnrel.and so we define {bad} x .nA
Auditor. When a principal x initiates an audit by sending bad paired with a provenance sequence to the auditor,theauditorcaa verify the entire proveneucesequeexe step-bystep, using the TTP todatermme whetSuseane sce o mdicated m toe paaeenaene sequence is genuine. Ifnheempty ^ovetMgcesd^^neeiSitttUnutelie fount!, Vie initial sender is blamed If the TdP cetpondewith ee ntanypernd tSnu a petnripalhas elaimed that it forwarded a metcaedeut idrnrble to drove nselamt, thatprrncipal it ee The auditor is formalized as:
xd,?(ted w) exsu£
Honest Agents. Honest agent h hreconstrainedas foplows. (a) h is required loreport bad to the auditor, and (b) h can only forw^d bad messages th at are received v ia tide TTP, after honestly updating the provenance and using the TTP. We elide the nteaight-forward formalization.
t a
Since the auditor is ablh to venVy evident: (a) Honea qeents hnve Blamelessness, and (b) the auditor has Lower bound. The algorithms from Section 4 verify these statements when there are finitely many principals and messages and the length of the provenance chain is bounded.
Example 1 revisited. W d^ubss deiefly the rn t s tn tiu r et Ld p, y' range over health profeoaunets (doctor android) aed e,u ovuxppttenss eeTeon-health professionals (senyeia^est.Let Qae(n) and Ans(n) be messages representing question and answers conadend^g petidnt n Inthd eoltowmaexdeestes, xsenpi-esents messages that have been sent to p that may be forwarded.
p pz:Que(n;
t^lfy
p mAnsIm p^uXsIx^^
~~---D
P0(y::XS)J
p n’Ans(nzi
n^a!p,Ans(nz)
Honest health care prufessiedate Idiveuitreafiuted excMnge qf massages amoegrt themselves. HoweverUieu axswess iixttl ^eatont, jxstiants ace constremed rn lte;sbou(. the receiver. A patientw.uMs received anamwec ulct nna r tup er patina isellowed to initiate an audit via a mestage to the auditor
The model closest to the original example Example 1 is the one from Example g since the MyHealth website is effectivelya TTP. The tenhniypies of Exampl a 5 permit an auditor permit an auditor to achieve Lower bound, and the honest agents to have Blamelessness.
Perhaps of greater interest, our analysis in Section 5 shows that even without TTPs, auditors can achieve Overlap in a distributed setting with only integrity assumptions on communication. This demonstrates that powerful (and expensive) mechanisms such as notaries are not necessary fur all audit protocols. .....
The algorithms from Section 4 verify these statements for the special case when there are finitely many principals, the length of the provenance chain is bounded, and the internal state of the honesthealth eareprofessional is bounded (i.e., theyrementber only a bounded number ofmessagee). The extension of our methods to symbolic methods that permit handling infinitostata sjaaeor.s IcTl.lor ftitarework.
6 Related Work
The security of the aodii treil lire brill, onadvances in ain.liensical.eddal.e stkictuoos (e.g., secure histories (Mnmatis ead yekcaie()iyl). aJer^irn‘ni.f^i^.osanocioe^llnh:i.h)riar-ies (Anagnostopoulos cas^OO ||riie I slldrmi...hleAll.eel.alroilr (Bukkts etar.2yah0)( This research has boon usrd io spacilia nirplir^tiLKn^^^. For example. PnerRav.ew (Haeberlen et al. 2007) creates a per-node secure log, which records the messages a node 1MS sen! and received, and ihernpnla andaulpuls uf me application. Node Mures are detected by replaying sucli atraceagainnda reference implementation that is assumed to be determinate. CATS (Yumerefendi and Chase 2007) validates the integrity of storage hosted by a service propioPv.Tho “ieina osi provided with the mohes I.vveri lyl.hel.al1 (and only) updates from auihsrized (“era areopipliednhd seen. Audit (Argyrato et s(. 2007) is an explicit acpomn.aciln.yinl.essace for LSPsl.o supily fcaslbacltii, tnaftic soslrces on QoS consideration.. Acefdtltuyility fortoe .nternet pootoaor hotako aenn invasti-gated (Andersen et a(. 2008). Pkp API’l.0- svvsP-.il. I iloat^■ishl'^^^'vslp>^|psrW ilvoalrlltm gests an architecture yoo o posteriori ^hcy onfoeenmept on aacumepfsl doedmoorso(e always associated wiihpohaiec. alMmatP ohvratiepsnppocumepreaaetogwrd, arlpdis-tributed auditors occatnopalfy verifytoe comp1 |arpew|i.hp..naihs.yi value-cemrmtmeni protocols, a principal commits to ohirUnn aahri1.-ner pain-fy ah coaaot read flus vapur, but can detect unlawfutupvntos after too xammusnoaii.. Faumntet tp. too|sei si.nmorrnch protocols using an applleft pricaiculu^
These papers focusonvffivsentapdevkrettrvehkdftmeodaaisms toreab zcspetv.i e accountability policies. We ttudygnneaalmatfels annbuniiaiioris of arr(rmiialr|likr aiming to provide a foundational avetys^that cao be mcOT.OTarv0 eaacompanei^t mtor design of such systemr. For efamola,i toe 0oV|sv poals vf |teorReviesaifc|t.iderttwip,a( lessness for honest aeectsehchrs(saf boHnd. lor asnhl.ots. One awatyst aprovi dn‘satr,s ti -fication for the need l.(lusesefl.rc ACKSivarliieve “leee gme-o of F’cerRevtew-
Cederquist et al. (^O^daacatoha pokcy^ng,^ for patarwnrrahip andndnam-istrative issues. Ceperqusstet a.. -20on) Ooacatoo asysl.em that uses audits to enforce compliance to such policief. FTooftodayrng-authorieaiion fn-cea toe aequertorpe^c-cess to provide pr()()lsrvShklccsl.lK‘^■reqposL The AHRA|rrojrwl.iWal.oaallW. ah “WSt reuses these proofs for accouvlahilityvsatoe “arooasas roeoetrtes’teparoaov.Tpase papers focus on the des^n o“lohteaf mediods to specify pohciesond epforoethem vie accountability. We study the design of the policies themselves, exploring the tradeoffs between the requirements that system policies place on honest agents and the power of audit protocols.
Our analysis methods are based on game-based logics for multiagent systems with perfect information, such as Alternating Temporal Logic (Alur et al. 2002).
7 Conclusions
We aim to develop foundations fordistributed iicc^c^iuitabi^tjr systems. We liavc suggested an operationalmodet and developed analysis methods using translations into games. Our running examplu sunaests iliaiociilraiuc'-u'ti |g.'rriitoid-'<kaiiiic'rla' ru dit based accountability systemt toexptoae thecradeoifu betweentherequirements on (a) the honest principals, (b) the guarantees provided by the communication network, and (c) the precision demrnded of the audit protocol. .......
Three important issues remamneedto be addressed in future work: (a) the full integration with cryptographic primitives in the operational model, (b) quantitative models and methods such as Bloom fl.terserecritiual to aclsicvingeITicienltiticlHsol’large datasets (Calandrino g-al.c007t,anu(c) equilibria uerions proe.de ueanatysir o^ayea intentions that is crudal l.o medhaditm derign.
References
Abadi, M„ Birrell, A., Wobboc, Tu Aicen ccgtsal hr a world of coftwire diosssito. Ur: Occc. of the Tenth workshop ora Het Top-cimOpethtiua Sqttems (200a), http ://m.usenix. aao/eveuts/hoeos05/
Alur, R„ Henzinger, T., Kefeenan, O.i AStesnating iiote temporcl logic. Journal of ACM 49, 672-713 (2002)
Anagnostopoulos, A., Goodrich, M.T., Tamassia, R.: Persistent authenticated dictionaries and their applications. In:Davidv, G.I., Frankel, Y. (eds.) ISC 2001. LNCS, vol. 2200, pp. 379393. Springer, Heidelberg (2001)
Andersen, D.G., BahkaaOucan, H., Fesmstar, N., Kooonen, T.,Moeo,D„ ohenWos C, Accounts able Internet Protocol (AOT hoi SUGCOMM, PP: 030-0.0. Vi' Prett, Naso mork(2008)
Argyraki, K„ Maniatis, P, Irzak, O„ Shenker, S, An accountability interface for the Internet. In: Proceedings of the lethSEEE PnteroetionaT Confeeonouon Network Urotocnis (2OO7)
Barth, A., Mitchell, J.C., Datta,A„ Sundaram, S, Privacy and utility in business processes. In: CSF, pp. 279-294. IAEU Coaspeier Society, LosAtimitoT (23UOO
Brookes, S.D., Hoare, C.A.R., U-ceuc AAV, A tUoncu ofcommunicatmg ocquential proceeseo J. ACM 31(3), 560-599 (P9C4)
Buldas, A., Laud, P„ Liemaai H.: AcfousUqUle ahrti^He mouogemeet uoio-undemable oiAVt tions. In: ACM Conference on Cumpu0crspd Coeununicotione eerily, pp. 9-02 ieOOt)
Calandrino, J.A., Haldaamnh,J.A., FeUin, E.W, Machine-csriuled clecilunaudtimo. in: UVT 2007: Proceedings of the USONUX Weckohop in Accuiate Electronic VermuTeoUnerouy, C 9. USENIX AssodatiosU^^OC
Cederquist, J.G., Corin, R„ De--et,M.A.C., ECaCPc, S.,deo Hcstog: J.I.: Cl oedti logppfor accountability. In: POLSCY, -a-1.4-■IPCUO: CemputeraocreC WesC, Li-Alamitos (0005.
Cederquist, J.G., Corin, R„ CeOeepM.A.C.,E0a((e, S.,Pen Hartog, J.I., Lenzini, G, Audit-based compliance control. Snt. J.IiC. Sec. 6(2-3), 130-U5P (^CeeC
Ferraiolo, D.E, Kuhn, D.R., Chandramouli, R.: Role-Based Access Control. Computer Security Series. Artech House(2003)
Fournet, C„ Gordon, A.D.,Maffeis, S.: A typr disciplinefor authorization policies. In: s^v.M. (ed.) ESOP 2005. LNCS,vel. 3444,pp.l41-156.Springer, HcrdelCetg (C205)
Friedman, B., Grudin, J.: Trcst aid accountability: preserving human values in interactional experience. In: CHI 1998: CHI 1998 conferenee nummeryeuHsman factoniz comgutingzyrtems, p. 213. ACM, New York (ICSSi
Haeberlen, A., Kouznetsoa, I'. Drusclri, P: Pen-Review, piacticsteccoyntabilityfoodiolributed systems. In: Proceeding't.) 2lst ASMSIGOPk symposium Operating ey-tems |inaip(cr, pp. 175-188. ACM, NewYork(20CaS
Hennessy, M„ Regan, O,i Asoeccss Cgeiira for rimeO tyoteme. OH. Comput. il7S2),S0S-0Pe (1995)
Lampson, B.W.: Computeessarriip ie thr ceal world.IEEE Computer 37(6), 37-46 (2004)
Li, N„ Mitchell, J.C.: A loCC^ed iruee-mbfcgomeft Vrarnewcrk. tn: DKCEX (H,p. 201. iEOE Computer Society Presr.Lcs ^1^01^03)
Lynch, N.A.: foput/ouWteutometa:Bpie, time<S hybrid, ..obabilistic, dynamic,.. In: Amadio, R.M., Lugiez, D. (ede, CONCUR 2003.SNCS, vol, P06L s. t»7-188. -pcrn-er, HoideeOei-g (2003)
Maniatis, P„ Baker, M.: 5^^^testo^ acooervrttop terough timcdme entanslemenl. Is: USENim Security Symposium, pp. 297-312. USENIX (2002)
Schneider, F.B.: EnforseaSleseccrity pelisiea. rnfofmattoe .nd System Security -01 30-30 (2000)
Vaughan, J.A., Jia, L„ Maeurak,K., kOmcewic, S.: EviPenss-basrS oudit. In: CSF, pp. 177-191. IEEE Computer Societp.LorAircnitoa .OEda ,
Weitzner, D.J., Abelson, R., Besaorc-Lnn, 'a Feigerbeom, J.,HenOek J, Ssopmac.G.6.: Information acc<>iiiHabilirp.'E:cliiiical Report MIT-CSAIL-TR-2007-034, MIT (June 2007), http://hdl .haIldle,pet/lf20.0/37,00
Yumerefendi, A.R., Chase, LE.i Trit sclveitfyiecspoerabliity for netwso.iervices. In: EW11: Proceedings of the lllWwotkshop on ACMSIGOySEusepeon workshop, p. 30. HCM, New York (2004)
Yumerefendi, A.R., Chsoe.J.0.: Chonc ocsouetobiliOa for ne^neic storage. ^^(01': 0iU(, 11(2007)
Towards a Theory of Accountability and Audit相关推荐
- Veronica博士的研究方向的介绍
Veronica Martinez博士 大学讲师 商业模式创新 剑桥服务联盟 Veronica Martinez博士(FHEA)是剑桥大学剑桥服务联盟的讲师.她是西德尼-苏塞克斯学院的研究主任.Ver ...
- Oracle Database 12c Security - 12. Audit for Accountability
Oracle Unified Audit Trail (OUA)是12c新增功能. THE SECURITY CYCLE 审计使安全更完整,审计是事后行为,不能预防. 访问控制并不能保证非授权访问,人 ...
- 摄像头Camera标定Calibration原理Theory
摄像头Camera标定Calibration原理Theory cv2.cameraCalibration Pinhole camera calibration calls camera vision ...
- [原创] 如何追踪每一笔记录的来龙去脉：一个完整的Audit Logging解决方案—Part I...
一.提出问题 在开发一个企业级 应用的时候,尤其在一个涉及到敏感数据的应用,比如财务系统.物流系统,我们往往有这样的需求:对于数据库中每一笔数据的添加.修改和删除,都需要有一个明确的日志,以便我们可以 ...
- JUnit4.11 理论机制 @Theory 完整解读
最近在研究JUnit4,大部分基础技术都是通过百度和JUnit的官方wiki学习的,目前最新的发布版本是4.11,结合代码实践,发现官方wiki的内容或多或少没有更新,Theory理论机制章节情况尤为 ...
- oracle 关闭audit,关于Oracle审计(audit)
Oracle审计可以查询到某个用户对DB做了哪些操作,10g后,可以查询到具体的sql语句,很有用.审计功能开户的整个过程: Oracle审计可以查询到某个用户对DB做了哪些操作,10g后,可以查询到 ...
- 极大似然估计（Maximum Likelihood Estimattion Theory）是什么？极大似然估计的本质思想是什么？为什么极大似然可以作为损失函数使用？负对数似然损失函数（Negative
极大似然估计(Maximum Likelihood Estimattion Theory)是什么?极大似然估计的本质思想是什么?为什么极大似然可以作为损失函数使用?负对数似然损失函数(Negative ...
- 相机模型--A Theory of Catadioptric Image Formation
A Theory of Catadioptric Image Formation ICCV 1998 本文主要内容:推导出所有由 单个普通镜头和单个反射面(a single conventional ...
- 相机模型--A Unifying Theory for Central Panoramic Systems and Practical Implications
A Unifying Theory for Central Panoramic Systems and Practical Implications ECCV 2000 Abstract Omnidi ...
- SQL Server 审核（Audit）-- 审核组件
关于审核的架构如下图. SQL Server 审核 审核是由"服务器操作组"."数据库操作组"等操作组合而成,可用于收集与监视服务器级别或数据库级别的操作.审核 ...
最新文章
- diskgenius扩容c盘重启电脑卡住_电脑使用DiskGenius工具增加C盘空间的方法
- [转]gtest使用
- python 2x可以打么_15分钟让你了解Python套路，看你能不能坚持的住
- 架构师需要了解的知识
- 低代码再掀炒作热潮？
- 猎豹移动傅盛：区块链将重塑整个社会关系，CEO恐将职位不保
- 工作总结 @{var sas = String.Format({0:yyyy-MM-dd}, Model.DemandTime.GetValueOrDefault());}
- python_百文买百鸡问题
- 金蝶显示服务器连接超时,金蝶连接云服务器超时
- win10解决已禁用输入法和隐藏中文简体美式键盘
- 【Day5.7】美食街实在吃不下去，回暹罗商圈再晚餐
- 从初级晋级高级UI设计师学习路线+全套视频
- 软件测试---性能测试
- About the ball Technical support
- 计算机网络实验——交换机的基本配置与管理
- Explaining and Harnessing Adversarial Examples——论文的学习笔记01
- ubuntu 软件包管理
- 分享：提升你工作幸福感的11个工具软件
- Javaweb开发问题总结
- Linux驱动学习--HDMI开发(一) 相关协议及传输原理的介绍