Formal validation of automated policy refinement in the management of network security systems

Policy hierarchies and automated policy refinement are powerful approaches to simplify administration of security services in complex network environments. A crucial issue for the practical use of these approaches is to ensure the validity of the policy hierarchy, i.e. since the policy sets for the lower levels are automatically derived from the abstract policies (defined by the modeller), we must be sure that the derived policies uphold the high-level ones. This paper builds upon previous work on Model-based Management, particularly on the Diagram of Abstract Subsystems approach, and goes further to propose a formal validation approach for the policy hierarchies yielded by the automated policy refinement process. We establish general validation conditions for a multi-layered policy model, i.e. necessary and sufficient conditions that a policy hierarchy must satisfy so that the lower-level policy sets are valid refinements of the higher-level policies according to the criteria of consistency and completeness. Relying upon the validation conditions and upon axioms about the model representativeness, two theorems are proved to ensure compliance between the resulting system behaviour and the abstract policies that are modelled.

Identifying the borders of mathematical knowledge

Based on a divide and conquer approach, knowledge about nature has been organized into a set of interrelated facts, allowing a natural representation in terms of graphs: each `chunk` of knowledge corresponds to a node, while relationships between such chunks are expressed as edges. This organization becomes particularly clear in the case of mathematical theorems, with their intense cross-implications and relationships. We have derived a web of mathematical theorems from Wikipedia and, thanks to the powerful concept of entropy, identified its more central and frontier elements. Our results also suggest that the central nodes are the oldest theorems, while the frontier nodes are those recently added to the network. The network communities have also been identified, allowing further insights about the organization of this network, such as its highly modular structure.

Metastable Periodic Patterns in Singularly Perturbed Delayed Equations

We consider the scalar delayed differential equation epsilon(x) over dot(t) = -x(t) + f(x(t-1)), where epsilon > 0 and f verifies either df/dx > 0 or df/dx < 0 and some other conditions. We present theorems indicating that a generic initial condition with sign changes generates a solution with a transient time of order exp(c/epsilon), for some c > 0. We call it a metastable solution. During this transient a finite time span of the solution looks like that of a periodic function. It is remarkable that if df/dx > 0 then f must be odd or present some other very special symmetry in order to support metastable solutions, while this condition is absent in the case df/dx < 0. Explicit epsilon-asymptotics for the motion of zeroes of a solution and for the transient time regime are presented.

The C(K, X) spaces for compact metric spaces K and X with a uniformly convex maximal factor

In this paper, we prove that if a Banach space X contains some uniformly convex subspace in certain geometric position, then the C(K, X) spaces of all X-valued continuous functions defined on the compact metric spaces K have exactly the same isomorphism classes that the C(K) spaces. This provides a vector-valued extension of classical results of Bessaga and Pelczynski (1960) [2] and Milutin (1966) [13] on the isomorphic classification of the separable C(K) spaces. As a consequence, we show that if 1 < p < q < infinity then for every infinite countable compact metric spaces K(1), K(2), K(3) and K(4) are equivalent: (a) C(K(1), l(p)) circle plus C(K(2), l(q)) is isomorphic to C(K(3), l(p)) circle plus (K(4), l(q)). (b) C(K(1)) is isomorphic to C(K(3)) and C(K(2)) is isomorphic to C(K(4)). (C) 2011 Elsevier Inc. All rights reserved.

On the Hamilton-Jacobi equation in the framework of generalized functions

In this work we study, in the framework of Colombeau`s generalized functions, the Hamilton-Jacobi equation with a given initial condition. We have obtained theorems on existence of solutions and in some cases uniqueness. Our technique is adapted from the classical method of characteristics with a wide use of generalized functions. We were led also to obtain some general results on invertibility and also on ordinary differential equations of such generalized functions. (C) 2011 Elsevier Inc. All rights reserved.

Towards a maximal extension of Pelczynski`s decomposition method in Banach spaces

l Suppose that X, Y. A and B are Banach spaces such that X is isomorphic to Y E) A and Y is isomorphic to X circle plus B. Are X and Y necessarily isomorphic? In this generality. the answer is no, as proved by W.T. Cowers in 1996. In the present paper, we provide a very simple necessary and sufficient condition on the 10-tuples (k, l, m, n. p, q, r, s, u, v) in N with p+q+u >= 3, r+s+v >= 3, uv >= 1, (p,q)$(0,0), (r,s)not equal(0,0) and u=1 or v=1 or (p. q) = (1, 0) or (r, s) = (0, 1), which guarantees that X is isomorphic to Y whenever these Banach spaces satisfy X(u) similar to X(p)circle plus Y(q), Y(u) similar to X(r)circle plus Y(s), and A(k) circle plus B(l) similar to A(m) circle plus B(n). Namely, delta = +/- 1 or lozenge not equal 0, gcd(lozenge, delta (p + q - u)) divides p + q - u and gcd(lozenge, delta(r + s - v)) divides r + s - v, where 3 = k - I - in + n is the characteristic number of the 4-tuple (k, l, m, n) and lozenge = (p - u)(s - v) - rq is the discriminant of the 6-tuple (p, q, r, s, U, v). We conjecture that this result is in some sense a maximal extension of the classical Pelczynski`s decomposition method in Banach spaces: the case (1, 0. 1, 0, 2. 0, 0, 2. 1. 1). (C) 2009 Elsevier Inc. All rights reserved.

NEW CHARACTERIZATIONS OF COMPLETE SPACELIKE SUBMANIFOLDS IN SEMI-RIEMANNIAN SPACE FORMS

In this paper we study n-dimensional complete spacelike submanifolds with constant normalized scalar curvature immersed in semi-Riemannian space forms. By extending Cheng-Yau`s technique to these ambients, we obtain results to such submanifolds satisfying certain conditions on both the squared norm of the second fundamental form and the mean curvature. We also characterize compact non-negatively curved submanifolds in De Sitter space of index p.

Algebraic Bol loops

In this paper, we study the category of algebraic Bol loops over an algebraically closed field of definition. On the one hand, we apply techniques from the theory of algebraic groups in order to prove structural theorems for this category. On the other hand, we present some examples showing that these loops lack some nice properties of algebraic groups; for example, we construct local algebraic Bol loops which are not birationally equivalent to global algebraic loops.

REALIZING PROFINITE REDUCED SPECIAL GROUPS

Special groups are an axiomatization of the algebraic theory of quadratic forms over fields. It is known that any finite reduced special group is the special group of some field. We show that any special group that is the projective limit of a projective system of finite reduced special groups is also the special group of some field.

SEMIPERFECT IPRI-RINGS AND RIGHT BEZOUT RINGS

We present a survey of some results on ipri-rings and right Bezout rings. All these rings are generalizations of principal ideal rings. From the general point of view, decomposition theorems are proved for semiperfect ipri-rings and right Bezout rings.

Protocols between programs and proofs

In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors, but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include 1. a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs when we obtain programs from formal proofs, and 2. a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other. An implementation of our methodology is the Fred system. As an example of our protocol we describe a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.

Evidence Algorithm and Processing Formalized Mathematical Texts

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

On choice of technique in the Robinson-Solow-Srinivasan model

We report results on the optimal \choice of technique" in a model originally formulated by Robinson, Solow and Srinivasan (henceforth, the RSS model) and further discussed by Okishio and Stiglitz. By viewing this vintage-capital model without discounting as a speci c instance of the general theory of intertemporal resource allocation associated with Brock, Gale and McKenzie, we resolve longstanding conjectures in the form of theorems on the existence and price support of optimal paths, and of conditions suÆcient for the optimality of a policy rst identi ed by Stiglitz. We dispose of the necessity of these conditions in surprisingly simple examples of economies in which (i) an optimal path is periodic, (ii) a path following Stiglitz' policy is bad, and (iii) there is optimal investment in di erent vintages at di erent times. (129 words)

Asset pricing when risk sharing is limited by default: a theoretical framework

We study the asset pricing implications of an endowment economy when agents can default on contracts that would leave them otherwise worse off. We specialize and extend the environment studied by Kocherlakota (1995) and Kehoe and Levine (1993) to make it comparable to standard studies of asset pricillg. We completely charactize efficient allocations for several special cases. We illtroduce a competitive equilibrium with complete markets alld with elldogellous solvency constraints. These solvellcy constraints are such as to prevent default -at the cost of reduced risk sharing. We show a version of the classical welfare theorems for this equilibrium definition. We characterize the pricing kernel, alld compare it with the one for economies without participation constraints : interest rates are lower and risk premia can be bigger depending on the covariance of the idiosyncratic and aggregate shocks. Quantitative examples show that for reasonable parameter values the relevant marginal rates of substitution fali within the Hansen-Jagannathan bounds.

A restatement of the welafare costs of inflation. The wast of scarce resources in the manufacturing , banking and household sectors

Lucas (2000) estimates that the US welfare costs of inflation are around 1% of GDP. This measurement is consistent with a speci…c distorting channel in terms of the Bailey triangle under the demand for monetary base schedule (outside money): the displacement of resources from the production of consumption goods to the household transaction time à la Baumol. Here, we consider also several new types of distortions in the manufacturing and banking industries. Our new evidences show that both banks and firms demand special occupational employments to avoid the inflation tax. We de…ne the concept of ”the foat labor”: The occupational employments that are aflected by the in‡ation rates. More administrative workers are hired relatively to the bluecollar workers for producing consumption goods. This new phenomenon makes the manufacturing industry more roundabout. To take into account this new stylized fact and others, we redo at same time both ”The model 5: A Banking Sector -2” formulated by Lucas (1993) and ”The Competitive Banking System” proposed by Yoshino (1993). This modelling allows us to characterize better the new types of misallocations. We …nd that the maximum value of the resources wasted by the US economy happened in the years 1980-81, after the 2nd oil shock. In these years, we estimate the excess resources that are allocated for every speci…c distorting channel: i) The US commercial banks spent additional resources of around 2% of GDP; ii) For the purpose of the firm foating time were used between 2.4% and 4.1% of GDP); and iii) For the household transaction time were allocated between 3.1% and 4.5 % of GDP. The Bailey triangle under the demand for the monetary base schedule represented around 1% of GDP, which is consistent with Lucas (2000). We estimate that the US total welfare costs of in‡ation were around 10% of GDP in terms of the consumption goods foregone. The big di¤erence between our results and Lucas (2000) are mainly due to the Harberger triangle in the market for loans (inside money) which makes part of the household transaction time, of the …rm ‡oat labor and of the distortion in the banking industry. This triangle arises due to the widening interest rates spread in the presence of a distorting inflation tax and under a fractionally reserve system. The Harberger triangle can represent 80% of the total welfare costs of inflation while the remaining percentage is split almost equally between the Bailey triangle and the resources used for the bank services. Finally, we formulate several theorems in terms of the optimal nonneutral monetary policy so as to compare with the classical monetary theory.