Eurosys2010draft
From AWiki
Contents |
Aktuálna verzia draftu
Zmeny oproti verzii, ktorá bola submitnutá na SOFSEM a odmietnutá
Zmenil som názov článku z Augmented Object-Capability Security Model na Toward Robust Software Systems. Myslím, že je to vhodnejší názov lebo priamo hovorí o tom, o čo mi ide. Neodvádza pozornosť. Takisto je asi výhodné sa v názve článku vyhnúť neobvyklým pojmom (object-capability security model, defensive correctness ap.). Dúfam, že to podľa názvu nebude považované za výťah z tejto dizertačky.
Zmenil som abstrakt. Pôvodný abstrakt obsahoval príliš veľa "cudzích slov" a viem si predstaviť, že toto nemajú ľudia radi (nechať sa hneď na začiatku zasypať rôznymi čudnými pojmami). Abstrakt som preto prepísal a snáď je OK.
Vynechal som tam ten svoj odkaz na Ka-Ping Yee-ov článok Firefighters and Engineers. Je zábavný, ale tak ako som ho citoval tam príliš nesedel a nechce sa mi rozmýšľať, ako to tam lepšie zapasovať. Až tak na tom nezáleží. Dá sa to vynechať, tak som to vynechal.
Vynechal som tam tú referenciu na Scheffler, Springer, Froehlich: Object-capability security in virtual environments. Týka sa zaujímavej oblasti, ale možno to odvádza pozornosť príliš ďaleko. (A som lenivý vymyslieť nejaký vhodnejší spôsob, ako to tam zaliesť).
Na prvej strane, v pravom stĺci je odstavec Object-capability programming languages enable us .... Toto som jemne upravil:
- Namiesto frázy an object-capability language design from scratch som tam dal an object-capability language by design.
- namiesto fráz tamed version of ... som tam dal retrofitted version of .... Súvis s tým, čomu my hovoríme taming som hodil len do poznámky pod čiarou. To je lokálny folklór.
Posledný odstavec sekcie 1 (Introduction) bol jemne doplnený. Aby nedošlo k omylu, zdôrazňujem, že svoje riešenie (ako umožniť tvorbu nielen defenzívne konzistentných ale aj defenzívne korektných) softvérových systémov som spravil pre zvolený programovací jazyk. Pre tento jazyk:
- mením sémantiku existujúcich konštrukcií
- a zavádzam nové nevyhnutné konštrukcie.
Sekciu 2 som preformuloval. Nehovorím o subsystémoch, ale o procesoch. Je to trochu konkrétnejší výraz. Vynechávam zmienky o POLA (nie je to definované a nechcem celú sekciu nerobiť nič iné len definovať nové pojmy). V novej verzii sa snažím poukázať na to, čím sú tie Milnerove procesy zaujímavé z pohľadu bezpečnosti---že tam vieme jednoducho vysledovať, ako môžu jednotlivé procesy ovplyvniť svoje okolie. Je tam (v poznámke pod čiarou) vysvetlené, prečo namiesto pojmu privilege používame slovo authority. Na konci sekcie je myslím vydarený opis súvisu pojmu defenzívna konzistentnosť s POLA.
Sekciu 3 som prepísal. Príliš tam teraz nerozpitvávam to, ako viem tvoriť proxy-procedúry. Toto je nádherná vec, môže to byť súčasťou vecí, ktoré ma motivujú, ale nie je nevyhnutné popisovať tu. Venujem sa len tomu, čo priamo súvisí s nadpisom tejto sekcie.
Sekciu 4 som prepísal. Zlepšenie spočíva čiastočne v tom, že som tam starostlivejšie zdôvodnil to, prečo som si vybral jazyk Pict a nepoužívam iné bežnejšie jazyky. Snažil som sa uviesť postačujúce konzervatívne dôvody namiesto nejakých krikľavých. Posledným odstavcom sa naväzujem na obsah ďalšej sekcie a zvyšku článku. Nech je to koherentné.
Sekcia 5:
- Pôvodný nadpis "An updated object-capability security model" som zmenil na "Weaknesses of the Pict programming language". Je asi menej príťažlivý, ale viac zodpovedá realite.
- Popis obrázka 1 som zmenil. Lepšie popisuje úlohu proxy procesov a to ako sa používajú v celom systéme.
- Podnadpisy "Scenario ..." som zmenil na "Denial of service attack ...".
- Prepísal som sekcie 5.1 a 5.2. Teraz obsahujú trochu rozvitejšie ukážky (ktoré aj niečo robia). Pridal som sekciu 5.3, ktorá obsahuje motiváciu pre donating send akciu.
Sekcia 6: Toto je nova sekcia. Venuje sa vlastnostiam pôvodného jazyk. V ideálnom prípade by som sem mohol dať aj definíciu pôvodného abstraktného stroja, z ktorého som vychádzal. Bohužiaľ, do článku sa mi to nezmestí, ale urobil som maximum pre to, aby si to čitateľ mohol dohľadať. Je asi naivné predpokladať, že revieweri si pozrú aj niečo iné ako submitnutý článok, ale iné tu neviem spraviť.
Sekcia 7: Kompletne popisuje novú verziu abstraktného stroja. Je to podobný text ako bol v tom článku na PLAS ale nie je to čistá kópia:
- Niektoré veci som z toho PLAS textu vynechal (tie domnienky (conjectures) a náznaky dôkazov, že tie domnienky sú správne). Toto sa mi do aktuálneho článku už nezmestilo a nechcel som tam pliesť všetko možné.
- Niektoré redukčné pravidlá sa mierne zmenili. Tieto zmeny sú v zapracované v článku.
Sekcia 8 (Validation): Ja nová. Popisuje akým spôsobom sa vieme pomocou navrhovaného jazyka vysporiadať s hrozbami, ktoré popisujem v sekciách 5.1, 5.2 a 5.3.
Sekcia 9 (Related work): Pridal som odkaz na Singularity. Aby bolo jasné, akú sadu problémov rieši ich "channel contracts" a čo sa sažím riešiť ja.
Posudky (zo SOFSEM-u)
Prvý posudok
This paper brings some interesting insights in the issue of robustness w.r.t. communicating (sub)systems, but is poorly organized and styled. The paper content as such is likely to be of interest to the conference audience, but the paper as such calls for a considerable revision.
Text som revidoval. Myslím, že je lepší. Či to stačí je otázka.
The comparison of POLA and formal methods in Section 2 is misleading as it compares two approaches at considerably different levels of abstraction.
Toto porovnanie som tam zrušil.
The claim at the start of Subsection 5.3 that "According to Figure 1, ClockMorph can invoke Timer's services." is not correct since all that Fig. 1 legend claims w.r.t. this is that ClockMorph relies on services provided by Timer. These are two considerably different notions!!!
Ten popisok k obrázku som doplnil tak, aby jasnejšie vysvetlil vzťahy medzi jednotlivými procesmi.
The issue of accounting to the sender or receiver in Subsection 5.3 is considerably trickier as one has to consider limits to resources to avoid eg unfair pricing and also abuse of exhaustive resources. These (and other) issues are more complex than touched upon.
Aby bolo jasné, že sme uvažovali aj iné scenáre než tie, ktoré sú popísané v článku, na dve vhodné miesta v článku som vložil odkaz do dokumentácie ku kompilátoru (Sekcia 10.4.8), kde rôzne scenáre rozoberám. Nie je to zvlášť čitateľný text, ale bez ohľadu na formu takúto sumarizáciu som potreboval. Tvorí motiváciu k tomu tvaru redukčných pravidiel, ktoré uvádzam. Aby bolo jasné, prečo majú taký tvar a nie iný.
I suggest a considerable reduction (in size and coverage) of Section 6.
Nie som si istý, či som urobil dobre, ale práve tú sekciu som rozšíril (teraz má číslo 7). V tomto rozsahu by mohla dávať zmysel. Kvôli SOFSEM-u som ju musel uviesť v skrátenom tvare.
Critical acronyms and concepts must be first instroduced and then used, eg - POLA is not explained at all. Note also that majority of security literature uses term "least privilege" and not "least authority". - Taming is only somewhat mentioned in Section 6, but used in Section 1. - Total correctness is not defined at all.
Dal som si záležať na tom, aby som tieto pojmy definoval. Miesto "taming" ale používam všeobecnejší výraz "retrofitting".
A considerable attention must be paid to basic proofreading (by a native speaker) - too many parts of the paper are simply illegible.
TODO
The paper is also hard to read w.r.t. its reliance on the documentation referenced as [12], this must be avoided and the reader should have the paper/work much better self-contained.
Čo som vedel v tomto smere spraviť som dúfam spravil. Ale v tomto smere som mal obmedzené možnosti. Bohužiaľ výsledkom práce Turnera a Pierce-a nie je jeden vzorec, ktorý mi stačí uviesť ale opis ich výsledku, z ktorého som vychádzal zaberie veľa miesta.
Typos and other minor issues: - The bulletpoints at the paper start once use a correct item ends with commas and period, and once not.
Toto je dúfam už konzistetné.
- References like 1 and 2 are a bit unclear.
Ten Ka-Ping Yee-ho článok je pekný, ale nie asi tá referencia je príliš voľne viazaná s mojou témou. Vynechal som. Tá Schefflerova práca by sa asi dala spomenúť v Related work. Zatiaľ som to tam nedal, lebo som ju nečítal, aj keď je asi zaujímavá.
Druhý posudok
The authors outline a work in which Turner's language Pict is extended with two constructs that provide flexible control on the allocation of memory quotas to processes and flexible policies to charge the incurred memory costs to agents or subsystems, e.g. servers. The first five sections present the detailed motivations for this extension, in relation with security and availability. The two new constructs and the associated reduction rules are described in the sixth section. The paper is well written (but it is not totally free from repetitions), and it presents reasonable motivations and language constructs. It would ideally fit for accompanying a Demo of the Sahara programming language. However, in my opinion, the paper is not relevant in the Theoretical Computer Science track of SOFSEM.
Tretí posudok
PAPER: 33 TITLE: Augmented Object-Capability Security Model In this paper the authors present an informal methodology for guaranteeing a property known as defensive correctness using object capabilities and memory limitations. This property has already been studied for synchronous communications, and the authors investigate the property for asynchronous communications. The authors give an example to try to demonstrate why using the Pict language directly only permits a safety property which is weaker than defensive correctness, known as defensive consistency. They go on to describe the modifications they made in their own language to permit extending the work to defensive correctness. Defensive correctness is defined as: - it is defensively consistent (safety property) - it is responsive (liveness property) Defensive consistency is defined as: - a subsystem is defensively consistent if it does not provide unexpected service regardless what its clients try to do Where a subsystem is defined as either a server in a client-server system or a peer in a peer-to-peer system. The authors continue to argue that in order to guarantee consistency one simply has to keep track of if an entity is trying use up lots of memory (cancer) or send lots of messages (spam). However in order to strengthen to correctness the authors claim that they simply need to introduce 'donating sends', where the receiver gives the sender permission to charge the memory usages or messages to the receiver. Whilst this does permit correctness in the examples shown this does seems to assume that server is well behaved. It seems possible that a server or peer which has been given permission to do donating send by one of its clients could make that client exceed its memory limit.
Toto je dobrý postreh. Do svojho dokumentu som do sekcie 10.4.8 (Discussion) pridal text: Currently, when servers receive donating capabilities, they can sink their clients. In a peer-to-peer system this would be a problem. In a client-server system (like those I consider) this is not a serious problem. Clients already rely on the correctness of servers. The fact that servers can sink them (via donating sends) does not make them significantly more vulnerable. In a peer-to-peer system we could overcome this problem by employing linear types. A peer holding a linear donating capability would be able to send a message only finite number of times.
The language of the paper is at times unclear, and there are numerous apparent inconsistencies or typos, as detailed in the minor comments. There doesn't seem to be a clear flow of reasoning through the paper explaining and justifying the approach. It is also unclear how much of the contribution of their language and constructs comes from [10].
V tom texte, ktorý som submitol na SOFSEM mi vznikla chyba, ktorá práve zahmlila tú hranicu, ktorú reviewer spomína. Je to smola.
Providing facilities to guarantee that we can discover and remove badly behaving entities from a multi-entity system is an important problem. It is not clear, however, how much this approach does solve that problem, for example due to the issue mentioned above with servers and donating sends.
Uvažoval som rôzne scenáre. Sú zosumarizované v sekcii 10.4.8 v dokumentácii. Pridal som tam aj návrh riešenia toho problému, ktorý spomínajú (ako posledný scenár). Okrem toho v sekcii "Conclusion and future work" hovorím, že som vykonal čiastočnú validáciu (do tej miery, do ktorej to v danej fázy ide). Píšem tiež, že na kompletnú validáciu je potrebné bohatší jazyk. Aspoň tak bohatý, ako pôvodný Pict.
[10] Turner, D.N.: The Polymorphic Pi-calculus: Theory and Implementation. PhD thesis, University of Edinburgh (1995) Minor Comments: Doesn't explain what "partial correctness" is, no ref, etc. p2 or "total correctness" p4
Toto bola prekvapujúca poznámka, lebo zámerne som použil pojmy, o ktorých som myslel, že sú všeobecne známe a nemusím ich teda definovať.
"we do not excluded" first paragraph p3 "It means that via lexical scoping rules is ensured ..." should this be "It means that via lexical scoping rules IT is ensured..."? p3 "However, if we choose right set of communication primitives used by clients" should this be "However, if we choose THE right set of communication primitives used by clients"? p4 What is all the talk about "update" or updating about(e.g. p6) ? I don't see any update mechanisms "resilience of a given system against malbehaving subsystems" p8: subsystems are supposed to be servers, and I thought you were trying to guarantee that a server (subsystem) would continue to be well behaved in the case of any misbehaviour on the part of clients (systems)? "It is a sequence of ready-to-run processes. Q, H, E, p^ω ⇓ Q , H , R at the bottom of each reduction rule tells that if we execute process p within abstract machine in state Q, H, R the state of the abstract machine changes to Q' , H' , R' ", p9 : why is E in such a reduction, as the basic configuration seems to be "Q, H, R" not "Q, H, E"? ADOUt-W' rule, p11: should the left hand part of the reduction have "x!$z" annotated with w rather than just a line?
Toto som opravil.
Štvrtý posudok
PAPER: 33 TITLE: Augmented Object-Capability Security Model This paper is about programming languages and models for security. I'm not an expert in this precise area but for me the paper is inadequately motivated and very discursive, presenting ideas rather than completed work, and not drawing a clear boundary between what is original research and what is existing work. The contribution of the paper is not clear and, finally, the standard of English is poor. I must suggest rejection.
