waashk/dblp huggingface dataset:
providing flexibility in information flow control for object oriented systems. abstract: this paper presents an approach to control information flow in object-oriented systems that takes into account, besides authorizations on objects, also how the information has been obtained and/or transmitted. these aspects are considered by allowing exceptions to the restrictions stated by the authorizations. exceptions are specified by means of waivers associated with methods. two kinds of waivers are supported: invoke-waivers, specifying exceptions applicable during a method's execution, and reply-waivers, specifying exceptions applicable to the information returned by a method. information flowing from one object into another object is subject to the different waivers of the methods enforcing the transmission. we formally characterize information transmission and flow in a transaction taking into consideration different interaction modes among objects. we then define security specifications, meaning authorizations and waivers, and characterize safe information flows. we formally define conditions whose satisfaction ensures absence of unsafe flows and present an algorithm enforcing these conditions.
towards automatic generation of vulnerability-based signatures. in this paper we explore the problem of creating vulnerability signatures. a vulnerability signature matches all exploits of a given vulnerability, even polymorphic or metamorphic variants. our work departs from previous approaches by focusing on the semantics of the program and vulnerability exercised by a sample exploit instead of the semantics or syntax of the exploit itself. we show the semantics of a vulnerability define a language which contains all and only those inputs that exploit the vulnerability. a vulnerability signature is a representation (e.g., a regular expression) of the vulnerability language. unlike exploitbased signatures whose error rate can only be empirically measured for known test cases, the quality of a vulnerability signature can be formally quantified for all possible inputs.
computer security training and education: a needs analysis. abstract: this paper examines, from an employer's perspective, the kind of education and training that today's computer security practitioners need. it suggests answers to three important questions: (1) what are we educating people to do? (2) what should be included in education and training programs? (3) what can industry do to help?.
defining noninterference in the temporal logic of actions. abstract: covert channels are a critical concern for multilevel secure (mls) systems. due to their subtlety, it is desirable to use formal methods to analyze mls systems for the presence of covert channels. this paper describes an approach for using abadi & lamport's (1993) temporal logic of actions (tla) to specify noninterference properties. in addition to providing a more intuitive definition of noninterference than previous attempts, this approach also supports the analysis of systems that do contain covert channels to demonstrate limitations on their exploitations. in relating the definition of noninterference given in this paper to prior definitions of noninterference, this paper discusses ways in which other definitions of noninterference can be formalized in tla, too. finally, this paper discusses how prior work on specification refinement and composition might be applied to the noninterference problem within the framework provided by tla.
integrity (i) codes: message integrity protection and authentication over insecure channels. inspired by unidirectional error detecting codes that are used in situations where only one kind of bit errors are possible (e.g., it is possible to change a bit "0" into a bit "1", but not the contrary), we propose integrity codes (i-codes) for a radio communication channel, which enable integrity protection of messages exchanged between entities that do not hold any mutual authentication material (i.e. public keys or shared secret keys). the construction of i-codes enables a sender to encode any message such that if its integrity is violated in transmission over a radio channel, the receiver is able to detect it. in order to achieve this, we rely on the physical properties of the radio channel. we analyze in detail the use of i-codes on a radio communication channel and we present their implementation on a mica2 wireless sensor platform as a "proof of concept". we finally introduce a novel concept called "authentication through presence" that can be used for several applications, including for key establishment and for broadcast authentication over an insecure radio channel. we perform a detailed analysis of the security of our coding scheme and we show that it is secure with respect to a realistic attacker model.
collaborative filtering with privacy. server-based collaborative ?ltering systems have been very successful in e-commerce and in direct recommendation applications. in future, they have many potential applications in ubiquitous computing settings. but today's schemes have problems such as loss of privacy, favoring retail monopolies, and with hampering diffusion of innovations. we propose an alternative model in which users control all of their log data. we describe an algorithm whereby a community of users can compute a public "aggregate " of their data that does not expose individual users' data. the aggregate allows personalized recommendations to be computed by members of the community, or by outsiders. the numerical algorithm is fast, robust and accurate. our method reduces the collaborative ?ltering task to an iterative calculation of the aggregate requiring only addition of vectors of user data. then we use homomorphic encryption to allow sums of encrypted vectors o be computed and decrypted without exposing individual data. we give veri?cation schemes for all parties in the computation. our system can be implemented with untrusted servers, or with additional infrastructure, as a fully peer-to-peer (p2p)system.
a framework for the evaluation of intrusion detection systems. classification accuracy in intrusion detection systems (idss) deals with such fundamental problems as how to compare two or more idss, how to evaluate the performance of an ids, and how to determine the best configuration of the ids. in an effort to analyze and solve these related problems, evaluation metrics such as the bayesian detection rate, the expected cost, the sensitivity and the intrusion detection capability have been introduced. in this paper, we study the advantages and disadvantages of each of these performance metrics and analyze them in a unified framework. additionally, we introduce the intrusion detection operating characteristic (idoc) curves as a new ids performance tradeoff which combines in an intuitive way the variables that are more relevant to the intrusion detection evaluation problem. we also introduce a formal framework for reasoning about the performance of an ids and the proposed metrics against adaptive adversaries. we provide simulations and experimental results to illustrate the benefits of the proposed framework.
a security model of dynamic labeling providing a tiered approach to verification. in the proposed mandatory access control model, arbitrary label changing policies can be expressed. the relatively simple model can capture a wide variety of security policies, including high-water marks, downgrading, separation of duties, and chinese walls. the model forms the basis for a tiered approach to the formal development of secure systems, whereby security verification can be spread across what makes up the reference monitor and the security requirement specification. the advantage of this approach is that once a trusted computing base (tcb) is in place, reconfiguring it for different security requirements requires verification of just the new requirements. we illustrate the approach with a number of examples, including one policy that permits high-level subjects to make relabeling requests on low-level objects; the policy is multilevel secure.
evaluation of intrusion detectors: a decision theory approach. abstract: this paper presents a method of analysis for evaluating intrusion detection systems. the method can be used to compare the performance of intrusion detectors, to evaluate performance goals for intrusion detectors, and to determine the best configuration of an intrusion detector for a given environment. the method uses a decision analysis that integrates and extends roc (receiver operating characteristics) and cost analysis methods to provide an expected cost metric. we provide general results and illustrate the method in several numerical examples that cover a range of detectors operating that meet a performance goal and two actual detectors operating in a realistic environment. we demonstrate that, contrary to common advice, the value of an intrusion detection system and the optimal operation of that system depend not only on the system's roc curve, but also on cost metrics and the hostility of the operating environment as summarized by the probability of intrusion. extensions of the method are outlined, and conclusions are drawn.
retrofitting legacy code for authorization policy enforcement. researchers have argued that the best way to construct a secure system is to proactively integrate security into the design of the system. however, this tenet is rarely followed because of economic and practical considerations. instead, security mechanisms are added as the need arises, by retrofitting legacy code. existing techniques to do so are manual and ad hoc, and often result in security holes. we present program analysis techniques to assist the process of retrofitting legacy code for authorization policy enforcement. these techniques can be used to retrofit legacy servers, such as x window, web, proxy, and cache servers. because such servers manage multiple clients simultaneously, and offer shared resources to clients, they must have the ability to enforce authorization policies. a developer can use our techniques to identify security-sensitive locations in legacy servers, and place reference monitor calls to mediate these locations. we demonstrate our techniques by retrofitting the x11 server to enforce authorization policies on its x clients.
deterring voluntary trace disclosure in re-encryption mix networks. an all too real threat to the privacy offered by a mix network is that individual mix administrators may volunteer partial tracing information to a coercer. while this threat can never be eliminated - coerced mix servers could simply be forced to reveal all their secret data - we can deter administrators from succumbing to coercive attacks by raising the stakes. we introduce the notion of a trace-deterring mix permutation to guarantee privacy, and show how it ensures that a collateral key (used for an arbitrary purpose) be automatically revealed given any end-to-end trace from input to output elements. however, no keying material is revealed to a party who simply knows what input element corresponds to what output element. our techniques are sufficiently efficient to be deployed in large-scale elections, thereby providing a sort of publicly verifiable privacy guarantee. their impact on the size of the anonymity set - while quantifiable - are not of practical concern.
what do we mean by entity authentication? abstract: the design of authentication protocols has proven to be surprisingly error-prone. we suggest that this is partly due to a language problem. the objectives of entity authentication are usually given in terms of human encounters while we actually implement message passing protocols. we propose various translations of the high-level objectives into a language appropriate for communication protocols. in addition, protocols are often specified at too low a level of abstraction. we argue that encryption should not be used as a general primitive as it does not capture the specific purpose for using a cryptographic function in aparticular protocol.
leap-frog packet linking and diverse key distributions for improved integrity in network broadcasts. we present two new approaches to improving the integrity of network broadcasts and multicasts with low storage and computation overhead. the first approach is a leapfrog linking protocol for securing the integrity of packets as they traverse a network during a broadcast, such as in the setup phase for link-state routing. this technique allows each router to gain confidence about the integrity of a packet before passing it on to the next router; hence, allows many integrity violations to be stopped immediately in their tracks. the second approach is a novel key predistribution scheme that we use in conjunction with a small number of hashed message authentication codes (hmacs), which allows end-to-end integrity checking as well as improved hop-by-hop integrity checking. our schemes are suited to environments, such as in ad hoc and overlay networks, where routers can share only a small number of symmetric keys. moreover, our protocols do not use encryption (which, of course, can be added as an optional security enhancement). instead, security is based strictly on the use of one-way hash functions; hence, our algorithms are considerably faster than those based on traditional public-key signature schemes. this improvement in speed comes with only modest reductions in the security for broadcasting, as our schemes can tolerate small numbers of malicious routers, provided they donýt form significant cooperating coalitions.
efficient intrusion detection using automaton inlining. host-based intrusion detection systems attempt to identify attacks by discovering program behaviors that deviate from expected patterns. while the idea of performing behavior validation on-the-fly and terminating errant tasks as soon as a violation is detected is appealing, existing systems exhibit serious shortcomings in terms of accuracy and/or efficiency. to gain acceptance, a numberof technical advances are needed. in this paper we focus on automated, conservative, intrusion detection techniques, i.e. techniques which do not require human intervention and do not suffer from false positives. we present a static analysis algorithm for constructing a flow- and context-sensitive model of a program that allows for efficient online validation. context-sensitivity is essential to reduce the number of impossible control-flow paths accepted by the intrusion detection system because such paths provide opportunities for attackers to evade detection. an important consideration for on-the-fly intrusion detection is to reduce the performance overhead caused by monitoring. compared to the existing approaches, our inlined automaton model (iam) presents a good tradeoff between accuracy and performance. on a 32k line program, the monitoring overhead is negligible. while the space requirements of a naive iam implementation can be quite high, compaction techniques can be employed to substantially reduce that footprint.
using memory errors to attack a virtual machine. we present an experimental study showing that softmemory errors can lead to serious security vulnerabilitiesin java and .net virtual machines, or in any system thatrelies on type-checking of untrusted programs as a protectionmechanism. our attack works by sending to the jvma java program that is designed so that almost any memoryerror in its address space will allow it to take controlof the jvm. all conventional java and .net virtual machinesare vulnerable to this attack. the technique of theattack is broadly applicable against other language-basedsecurity schemes such as proof-carrying code.we measured the attack on two commercial java virtualmachines: sun's and ibm's. we show that a single-biterror in the java program's data space can be exploitedto execute arbitrary code with a probability ofabout 70%, and multiple-bit errors with a lower probability.our attack is particularly relevant against smart cardsor tamper-resistant computers, where the user has physicalaccess (to the outside of the computer) and can usevarious means to induce faults; we have successfully usedheat. fortunately, there are some straightforward defensesagainst this attack.
analysis of the linux random number generator. linux is the most popular open source project. the linux random number generator is part of the kernel of all linux distributions and is based on generating randomness from entropy of operating system events. the output of this generator is used for almost every security protocol, including tls/ssl key generation, choosing tcp sequence numbers, and file system and email encryption. although the generator is part of an open source project, its source code (about 2500 lines of code) is poorly documented, and patched with hundreds of code patches. we used dynamic and static reverse engineering to learn the operation of this generator. this paper presents a description of the underlying algorithms and exposes several security vulnerabilities. in particular, we show an attack on the forward security of the generator which enables an adversary who exposes the state of the generator to compute previous states and outputs. in addition we present a few cryptographic flaws in the design of the generator, as well as measurements of the actual entropy collected by it, and a critical analysis of the use of the generator in linux distributions on diskless devices.
filtering postures: local enforcement for global policies. a abstract: when packet filtering is used as a security mechanism, different routers may need to cooperate to enforce the desired security policy. it is difficult to ensure that they will do so correctly. we introduce a simple language for expressing global network access control policies of a kind that filtering routers are capable of enforcing. we then introduce an algorithm that, given the network topology, will compute a set of filters for the individual routers; these filters are guaranteed to enforce the policy correctly. since these filters may not provide optimal service, a human must sometimes alter them. a second algorithm compares a resulting set of filters to the global network access control policy to determine all policy violations, or to report that none exist. a prototype implementation demonstrates that the algorithms are efficient enough to give quick answers to questions of realistic scale.
authentication tests. suppose a principal in a cryptographic protocol creates and transmits a message containing a new value v, which it later receives back in cryptographically altered form. it can conclude that some principal possessing the relevant key has transformed the message containing v. in some circumstances, this must be a regular participant of the protocol, not the penetrator. an inference of this kind is an authentication test. we introduce two main kinds of authentication test. an outgoing test is one in which the new value v is transmitted in encrypted form, and only a regular participant can extract it from that form. an incoming test is one in which v is received back in encrypted form, and only a regular participant can put it in that form. we combine these two tests with a supplementary idea, the unsolicited test, and a related method for checking that certain values remain secret. together, they determine what authentication properties are achieved by a wide range of cryptographic protocols. in this paper, we introduce authentication tests and illustrate their power, giving new and straightforward proofs of security goals for several protocols. we also illustrate how to use the authentication tests as a heuristic for finding attacks against incorrect protocols. finally, we suggest a protocol design process. we express these ideas in the strand space formalism [21], and prove them correct elsewhere [8].
an experience using two covert channel analysis techniques on a real system design. this paper examines the application of two covert channel analysis techniques to a high level design for a real system, the honeywell secure ada® target (sat). the techniques used were a version of the noninterference model of multilevel security due to goguen and meseguer and the shared resource matrix method of kemmerer. both techniques were applied to the gypsy abstract model of the sat. the paper discusses the application of the techniques and the nature of the covert channels discovered. the relative strengths and weaknesses of the two methods are discussed and criteria for an ideal covert channel tool are developed.
catalytic inference analysis: detecting inference threats due to knowledge discovery. knowledge discovery in databases can be enhanced by introducing "catalytic relations" conveying external knowledge. the new information catalyzes database inference, manifesting latent channels. catalytic inference is imprecise in nature, but the granularity of inference may be fine enough to create security compromises. catalytic inference is computationally intensive. however, it can be automated by advanced search engines that gather and assemble knowledge from information repositories. the relentless information gathering potential of such search engines makes them formidable security threats.this paper presents a formalism for modeling and analyzing catalytic inference in "mixed'' databases containing various precise, imprecise and fuzzy relations. the inference formalism is flexible and robust, and well-suited to implementation.
muse : a computer assisted verification system. muse is a verification system which extends the collection of tools developed by sri international for their hierarchical development methodology (hdm). it enhances the sri system by providing a capability for proving invariants and constraints for the state machine described by a specification written in special (the specification language of hdm). in particular, it enables one to use the hdm system to meet the requirements for formal verification in a national computer security center a1 evaluation of a secure operating system. in addition to the tools provided by sri, muse has a parser, a facility to handle multiple modules, a formula generator, and a theorem prover. the theorem prover has a number of interesting features designed to facilitate human direction of the proving process. in concept, it is open-ended. we introduce the notion of a theorem prover kernel as a device for ensuring the logical soundness of the prover in the face of continual improvements to its functionality.
practical attacks on proximity identification systems (short paper). the number of rfid devices used in everyday life has increased, along with concerns about their security and user privacy. this paper describes our initial findings on practical attacks that we implemented against 'proximity' (iso 14443 a) type rfid tokens. focusing mainly on the rf communication interface we discuss the results and implementation of eavesdropping, unauthorized scanning and relay attacks. although most of these attack scenarios are regularly mentioned in literature little technical details have been published previously. we also present a short overview of mechanisms currently available to prevent these attacks.
performance of public-key-enabled kerberos authentication in large networks. abstract: several proposals have been made to public-key-enable various stages of the secret-key-based kerberos network authentication protocol. the computational requirements of public key cryptography are much higher than those of secret key cryptography, and the substitution of public key encryption algorithms for secret key algorithms impacts performance. this paper uses closed, class-switching queuing models to demonstrate the quantitative performance differences between pkcross and pktapp-two proposals for public-key-enabling kerberos. our analysis shows that, while pktapp is more efficient for authenticating to a single server, pkcross outperforms the simpler protocol if there are two or more remote servers per remote realm. this heuristic can be used to guide a high-level protocol that combines both methods of authentication to improve performance.