1: \documentclass{llncs}

2: 

3: 

4: \usepackage{epsfig}

5: \usepackage{citesort}

6: \usepackage{fancybox,epic}

7: \usepackage{latexsym,amssymb}

8: 

9: \renewcommand{\topfraction}{1}

10: \renewcommand{\textfraction}{0.05}

11: \renewcommand{\floatpagefraction}{1}

12: 

13: 

14: \newcommand{\arestrict}{\mbox{\sf Arestrict}}

15: \newcommand{\aextend}{\mbox{\sf Aextend}}

16: \newcommand{\aunif}{\mbox{\sf Aunif}}

17: \newcommand{\aconj}{\mbox{\sf Aconj}}

18: \newcommand{\alub}{\mbox{\sf Alub}}

19: \newcommand{\acalltoentry}{\mbox{\sf Atranslate}}

20: \newcommand{\removeuselesscalls}{\mbox{\sc remove\_useless\_calls}}

21: 

22: 

23: \newcommand{\at}{\mbox{{$\cal AT$}}}

24: \newcommand{\atdisk}{\mbox{$AT_{disk}$}}

25: \newcommand{\datdisk}{\mbox{$DAT_{disk}$}}

26: \newcommand{\pdisk}{\mbox{$P_{disk}$}}

27: \newcommand{\dt}{\mbox{{$\cal DT$}}}

28: \newcommand{\gt}{\mbox{{$\cal GT$}}}

29: \newcommand{\st}{\mbox{{$\cal ST$}}}

30: \newcommand{\emptytable}{\mbox{\sf Create\_Table}}

31: \newcommand{\store}{\mbox{\sf Insert}}

32: \newcommand{\isin}{\mbox{\sf IsIn}}

33: \newcommand{\consult}{\mbox{\sf Look\_up}}

34: 

35: \newcommand{\newpred}{\mbox{\sf new\_filter}}

36: \newcommand{\renameheads}{\mbox{\sf rename\_heads}}

37: \newcommand{\ren}{\mbox{\sf ren}}

38: \newcommand{\getbody}{\mbox{\sf get\_body}}

39: \newcommand{\member}{\mbox{\sf Member}}

40: \newcommand{\delete}{\mbox{\sf Delete}}

41: 

42: \newcommand{\strategy}{\Omega}

43: 

44: \def\dep#1{\langle{#1}\rangle}

45: 

46: \newcommand{\aabstraction}{\mbox{\it AGeneralize}}

47: \newcommand{\aunfold}{\mbox{\it AUnfold}}

48: \newcommand{\abstraction}{\mbox{\it Generalize}}

49: \newcommand{\unfold}{\mbox{\it Unfold}}

50: 

51: \newcommand{\widencall}{\mbox{\it Widen\_Call}}

52: 

53: \newcommand{\adom}{{\it ADom}}

54: \newcommand{\aint}{{\it AInt}}

55: \newcommand{\aatom}{{\it AAtom}}

56: \newcommand{\acert}{{\it ACert}}

57: \newcommand{\dom}{D_\alpha}

58: \newcommand{\inten}{I_\alpha}

59: \newcommand{\atom}{S_\alpha}

60: \newcommand{\cert}{Cert_\alpha}

61: 

62: \newcommand{\certdel}{Cert_\alpha^{del}}

63: \newcommand{\certch}{Cert_\alpha^{ch}}

64: \newcommand{\certadd}{Cert_\alpha^{add}}

65: 

66: 

67: \newcommand{\qhs}{QHS}

68: 

69: \newcommand{\lsem}{\mbox{$\lbrack\hspace{-0.3ex}\lbrack$}}

70: \newcommand{\rsem}{\mbox{$\rbrack\hspace{-0.3ex}\rbrack$}}

71: \newcommand{\sqbrack}[1]{\lsem #1 \rsem}

72: \newcommand{\Inten}{\mbox{$\cal I$}}

73: \newcommand{\intabs}{\mbox{${\cal I}_{\alpha^+}$}}

74: \newcommand{\p}{{\sqbrack{P}}}

75: 

76: \newcommand{\sem}[1]{S_{#1}}

77: \newcommand{\semabs}{\p_\alpha}

78: 

79: %% from TOPLAS2000

80: \newcommand{\CP}{\mbox{\it CP}}

81: \newcommand{\defff}{\mathit{Def}}

82: \newcommand{\AP}{\mbox{\it AP}}

83: 

84: 

85: \newcommand{\algorithmicinput}{\textbf{Input:~}}

86: \newcommand{\algorithmicoutput}{\textbf{Output:~}}

87: \newcommand{\algorithmicglobal}{\textbf{Global:~}}

88: 

89: \newcommand{\short}[1]{}

90: \newcommand{\mycomment}[1]{\textbf{*** #1 ***}}

91: \newcommand{\sidenote}[1]{\marginpar{#1}}

92: %% Elvira's macros

93: \newcommand{\lub}{\sqsubseteq}

94: \long\def\comment#1{}

95: 

96: %% from DISCIPL

97: \newcommand{\kbd}[1]{\mbox{\tt #1}}

98: \newcommand{\nt}[1]{\mbox{\it #1}}

99: 

100: %% from LOPSTR99

101: \newcommand{\Q}{\mbox{$\cal Q$}}

102: \def\tuple#1{\langle{#1}\rangle}

103: 

104: %% NEW

105: \newcommand{\calls}{\mathit{calls}}

106: \newcommand{\success}{\mathit{success}}

107: \newcommand{\ciao}{\texttt{Ciao}}

108: \newcommand{\ciaopp}{\texttt{CiaoPP}}

109: \newcommand{\trismall}{{\scriptsize \vartriangleright}}

110: \newcommand{\Proof}{\sf{Cert}}

111: \newcommand{\certificate}{\sf{Cert}}

112: 

113: \newcommand{\cpcheck}{${\it CP_{\it checked}}$}

114: \newcommand{\cptocheck}{${\it CP_{\it tocheck}}$}

115: \newcommand{\cpunchange}{${\it propagate}$}

116: 

117: 

118: \newcommand{\entry}[2]{#1 \mapsto #2}

119: \newcommand{\cparc}[2]{#1 \# #2}

120: \newcommand{\dependency}[2]{#1 \Rightarrow #2}

121: 

122: \newcommand{\certifier}{{\sf cer\-ti\-fi\-er}}

123: \newcommand{\ext}[1]{\mathit{Ext_{#1}}}

124: \newcommand{\del}[1]{\mathit{Del_{#1}}}

125: \newcommand{\Mod}[1]{\mathit{{\it Upd}({#1})}}

126: 

127: \newcommand{\addition}[1]{\mathit{Add(#1)}}

128: \newcommand{\deletion}[1]{\mathit{Del(#1)}}

129: 

130: 

131: \newcommand{\analyzerA}{{\sc Analyze}}

132: \newcommand{\certifierA}{{\sc Inc\_Certifier}}

133: \newcommand{\checkerA}{{\sc Incr\_Che\-cker}}

134: \newcommand{\checkingA}{{\sc Checking}}

135: \newcommand{\extendprog}{{\sc Extend\_Prog}}

136: \newcommand{\extendcert}{{\sc Extend\_Cert}}

137: 

138: \newcommand{\certificateA}{{\sf Cert}}

139: 

140: \newcommand{\prog}{{\sf P}}

141: \newcommand{\eprog}{\it U_P} %{\sf Upd\_P}}

142: \newcommand{\ok}{{\sc OK}}

143: \newcommand{\valid}{{\sc Valid}}

144: 

145: 

146: \newcommand{\analyzerB}{{\sc Analyze\_r}}

147: \newcommand{\certifierB}{{\sc Certifier\_r}}

148: \newcommand{\checkerB}{{\sc Checker\_r}}

149: \newcommand{\certificateB}{{\sf In\-c\_\-Ce\-rt}}

150: \newcommand{\addcert}{{\sf Add\_Cert}}

151: \newcommand{\delcert}{{\sf Del\_Cert}}

152: 

153: \newcommand{\checkingB}{{\sc Checking\_r}}

154: \newcommand{\certificateL}{{\sf Ext\-\_\-Ce\-rt}}

155: 

156: 

157: \newcommand{\error}{{\sf Error}}

158: \newcommand{\true}{{\sf True}}

159: 

160: \newcommand{\false}{{\sf False}}

161: 

162: 

163: 

164: \renewcommand{\odot}{\oplus}

165: 

166: 

167: \begin{document}

168: 

169: \title{Some Issues on Incremental Abstraction-Carrying Code}

170: 

171: 

172: 

173: 

174: \author{Elvira Albert\inst{1} \and Puri Arenas\inst{1} \and Germ\'{a}n

175:   Puebla\inst{2}}

176: 

177: \institute{Complutense University of Madrid,

178: \email{\{elvira,puri\}@sip.ucm.es}

179: \and

180: Technical University of Madrid,

181: \email{german@fi.upm.es}

182: }

183: 

184: 

185: 

186: 

187: \maketitle

188: 

189: 

190: 

191: 

192: 

193: 

194: \begin{abstract}

195: 

196:   \emph{Abstraction-Carrying Code} (ACC) has recently been proposed as

197:   a framework for proof-carrying code (PCC) in which the code supplier

198:   provides a program together with an \emph{abstraction} (or abstract

199:   model of the program) whose validity entails compliance with a

200:   predefined safety policy. The abstraction thus plays the role of

201:   safety certificate and its generation (and validation) is carried

202:   out automatically by a fixed-point analyzer.  Existing

203:   approaches for PCC are developed under the assumption that the

204:   consumer reads and validates the entire program w.r.t.\ the

205:   \emph{full} certificate at once, in a non incremental way.  In this

206:   abstract, we overview the main issues on \emph{incremental} ACC. In

207:   particular, in the context of logic programming, we discuss both the

208:   generation of incremental certificates and the design of an

209:   incremental checking algorithm for untrusted \emph{update}s of a

210:   (trusted) program, i.e., when a producer provides a modified version

211:   of a previously validated program. By update, we refer to any

212:   arbitrary change on a program, i.e., the extension of the program

213:   with new predicates, the deletion of existing predicates and the

214:   replacement of existing predicates by new versions for them. We also

215:   discuss how each kind of update affects the incremental extension in

216:   terms of accuracy and correctness.

217: 

218: 

219: \end{abstract}

220: 

221: \section{Introduction}

222: 

223: 

224: 

225: Proof-Carrying Code (PCC) \cite{Nec97} is a general technique for

226: mobile code safety which proposes to associate safety information in

227: the form of a \emph{certificate} to programs. The certificate (or

228: proof) is created at compile time by the \emph{certifier} on the code

229: supplier side, and it is packaged along with the code.  The consumer

230: who receives or downloads the (untrusted) code+certificate package can

231: then run a \emph{checker} which by an efficient inspection of the code

232: and the certificate can verify the validity of the certificate and

233: thus compliance with the safety policy.  The key benefit of this

234: ``certificate-based'' approach to mobile code safety is that the

235: consumer's task is reduced from the level of proving to the level of

236: checking, a task which should be much simpler, efficient, and automatic

237: than generating the original certificate.

238: 

239: Abstraction-carrying code (ACC) \cite{lpar04-ai-safety} has been

240: recently proposed as an enabling technology for PCC in which an

241: \emph{abstraction} (i.e., an abstract model of the program) plays the

242: role of certificate. An important feature of ACC is that not only the

243: checking, but also the generation of the abstraction (or fixpoint) is

244: \emph{automatically} carried out by a fixed-point analyzer.

245: Lightweight bytecode verification \cite{RR98} is another PCC method

246: which relies on analysis techniques (namely on type analysis in the

247: style of those used for Java bytecode verification \cite{JVM03}) to

248: generate and check certificates in the context of the Java Card

249: language. In this paper, we will consider analyzers which construct a

250: program \emph{analysis graph} which is interpreted as an abstraction

251: of the (possibly infinite) set of states explored by the concrete

252: execution.  Essentially, the certification/analysis carried out by the

253: supplier is an iterative process which repeatedly traverses the

254: analysis graph until a fixpoint is reached.  A key idea in ACC is

255: that, since the certificate is a fixpoint, a single pass over the

256: analysis graph is sufficient to validate the certificate in the

257: consumer side. 

258: 

259: Existing models for PCC (ACC among them) are based on checkers which

260: receive a ``certificate+program'' package and read and validate the

261: entire program w.r.t.\ its certificate at once, in a non incremental

262: way.  However, there are situations which are not well suited to this

263: simple model and which instead require only rechecking certain parts

264: of the analysis graph which has already been validated. In particular,

265: we consider possible untrusted \emph{updates} of a validated (trusted)

266: code, i.e., a code producer can (periodically) send to its consumers

267: new updates of a previously submitted package. We characterize the

268: different kind of updates, or modifications over a program.  In

269: particular, we include: 

270: 

271: \begin{enumerate}

272: \item the \emph{addition} of new data/predicates

273: and the extension of already existing predicates with new

274: functionalities, 

275: \item the \emph{deletion} of predicates or parts of them

276: and 

277: \item the \emph{replacement} of certain (parts of) predicates by new

278: versions for them. 

279: \end{enumerate}

280: 

281: In such a context of frequent software updates, it appears inefficient

282: to submit a full certificate (superseding the original one) and to

283: perform the checking of the entire updated program from scratch, as

284: needs to be done with current systems.  In the context of ACC, we

285: discuss the influence of the different kinds of updates on an

286: \emph{incremental} extension to PCC in terms of correctness and

287: efficiency. We also outline the main issues on the generation of

288: incremental certificates and the design of incremental checkers.

289: 

290: 

291: The paper is organized as follows. Section

292: \ref{sec:basics-abstr-carry} introduces briefly some notation and

293: preliminary notions on abstract interpretation and ACC. In Section

294: \ref{sec:incremental-acc}, we present a general view of incremental

295: ACC.  In Section \ref{cu} we describe the different kinds of updates

296: over a program and the way they affect the certification and checking

297: phases.  Section \ref{icertificates} reviews the notion of full

298: certificate and proposes the use of incremental certificate.  In

299: Section \ref{icheckers}, we discuss the extensions needed on a

300: non-incremental checking algorithm in order to support incrementality

301: and we sketch the new tasks of an incremental checking algorithm.

302: Finally, Section~\ref{sec:discussion} concludes.

303: 

304: 

305: 

306: \section{Abstraction-Carrying Code}

307: \label{sec:basics-abstr-carry}

308: 

309: Our work relies on the abstract interpretation-based analysis

310: algorithm of \cite{incanal-toplas} for (Constraint) Logic Programming,

311: (C)LP. We assume some familiarity with abstract interpretation (see

312: \cite{Cousot77}), (C)LP (see, e.g.,

313: \cite{Lloyd87,marriot-stuckey-98})  and PCC \cite{Nec97}.  

314: 

315: Very briefly, {\em terms} are

316: constructed from variables (e.g., $x$), {\em functors} (e.g., $f$) and

317: {\em predicates} (e.g., $p$). We denote by $\{x_1 \mapsto t_1, \ldots,

318: x_n \mapsto t_n\}$ the {\em substitution} $\sigma$, where $x_i \not =

319: x_j$, if $i \not = j$, and $t_i$ are terms. A {\em renaming} is a

320: substitution $\rho$ for which there exists the inverse $\rho^{-1}$

321: such that $\rho \rho^{-1} \equiv \rho^{-1} \rho \equiv {\it id}$. A

322: {\em constraint} is a conjunction of expressions built from predefined

323: predicates (such as inequalities over the reals) whose arguments are

324: constructed using predefined functions (such as real addition). An

325: {\em atom} has the form $p(t_1,...,t_n)$ where $p$ is a predicate

326: symbol and $t_i$ are terms.  A {\em literal} is either an atom or a

327: constraint.

328: A {\em rule} is of the form $H \mbox{\tt :-} D$ where $H$, the {\em

329:   head}, is an atom and $D$, the {\em body}, is a possibly empty

330: finite sequence of literals.  A {\em constraint logic program} $P \in

331: {\it Prog}$, or {\em program}, is a finite set of rules.  Program rules are

332: assumed to be normalized: only distinct variables are allowed to occur

333: as arguments to atoms. Furthermore, we require that each rule defining

334: a predicate $p$ has identical sequence of variables $x_{p_1}, \ldots

335: x_{p_n}$ in the head atom, i.e., $p(x_{p_1}, \ldots x_{p_n})$.  We

336: call this the {\em base form} of $p$. This is not restrictive since

337: programs can always be normalized. 

338: 

339: 

340: An abstract interpretation-based certifier is a function {\sc

341:   Cer\-ti\-fi\-er}$:{\it Prog} \times \adom \times \aint \mapsto \acert$

342: which for a given program $P \in {\it Prog}$, an abstract domain $\dom

343: \in \adom$ and an abstract safety policy $\inten \in \aint$ generates

344: an abstract certificate $\cert \in \acert$, by using an abstract

345: interpreter for $\dom$, such that the certificate

346: entails that $P$ satisfies $\inten$. An

347: abstract safety policy $\inten$ is a specification of the safety

348: requirements given in terms of the abstract domain $\dom$. In

349: the following, using the same subscript

350: $\alpha$,  we denote that $\inten$ and $\cert$ are specifications

351: given as abstract semantic values of $\dom$.

352: 

353: The basics

354: for defining such certifiers (and their corresponding checkers) in ACC

355: are summarized in the following five points:

356: 

357: \begin{description}

358: 

359: 

360: \item[{\textbf{\em Approximation.}}] 

361: We consider a {\em description (or abstract)

362:   domain} $\langle \dom, \sqsubseteq \rangle \in \adom$ and its corresponding

363: \emph{concrete domain} $\langle 2^D, \subseteq \rangle$, both with a

364: complete lattice structure.  Description (or abstract) values and sets of concrete

365: values are related by an {\em abstraction} function $\alpha:

366: 2^{D}\rightarrow \dom$, and a {\em concretization} function $\gamma:

367: \dom\rightarrow 2^{D}$.  

368: The pair $\langle \alpha, \gamma \rangle$ forms a Galois

369:   connection. 

370:  The concrete and abstract domains must be related in such a way that

371:   the following condition holds~\cite{Cousot77} 

372:   

373:   \[\forall x\in 2^D:~

374:   \gamma(\alpha(x)) \supseteq x \mbox{~~~and~~~} \forall y\in

375:   \dom:~ \alpha(\gamma(y)) = y \]

376: 

377: 

378: \noindent

379: In general $\sqsubseteq$ is induced by $\subseteq$ and $\alpha$.

380: Similarly, the operations of {\em least upper bound\/} ($\sqcup$) and

381: {\em greatest lower bound\/} ($\sqcap$) mimic those of $2^D$ in a

382: precise sense.

383: 

384: \medskip

385: 

386: \item[{\textbf{\em Analysis.}}] We consider the class of {\em fixed-point semantics}

387:   in which a (monotonic) semantic operator, $S_P$, is associated to

388:   each program $P$.

389:   The meaning of the program, $\lsem P \rsem$,

390:   is defined as the least fixed point of the $S_P$ operator, i.e.,

391:   $\lsem P \rsem = {\rm lfp}(S_P)$.  If $S_P$ is continuous, the least

392:   fixed point is the limit of an iterative process involving at most

393:   $\omega$ applications of $S_P$ starting from the bottom element

394:   of the lattice. Using abstract interpretation, we can usually only

395:   compute $\p_\alpha$, as $\p_\alpha={\rm lfp}(S_P^\alpha)$.

396:   The operator $S_P^\alpha$ is the abstract counterpart of $S_P$.

397: 

398: 

399: \begin{equation}\label{eq:1} {\sf analyzer}(P,\dom) = {\rm

400:     lfp}(S_P^\alpha) = \p_\alpha

401: \end{equation}

402: %

403: Correctness of analysis ensures that $\semabs$ safely approximates

404: $\sqbrack{P}$, i.e., $\sqbrack{P}\in \gamma(\sqbrack{P}_\alpha)$.

405: Thus, such \emph{abstraction} can be used as a certificate.

406: 

407: \medskip

408: 

409: 

410: 

411: \item[{\textbf{\em Certificate.}}]

412: Let $\cert$ be a safe approximation of $\semabs$.

413:   If an abstract safety specification $\inten$ can be proved w.r.t.\

414:   $\cert$, then $P$ satisfies the safety

415:   policy and $\cert$ is a valid certificate:

416: 

417: 

418: \begin{equation}\label{ecuacion2}

419: \cert \mbox{ is \emph{a valid certificate} for $P$ w.r.t. }

420:  \inten \mbox{ iff }

421:     \cert \sqsubseteq \inten

422: \end{equation}

423:   

424: 

425: 

426: \noindent

427: Note that the certificate can be stricter than the

428: safety specification and it is only required that $\inten$ is implied

429: by $\cert$.

430: 

431: \medskip

432: 

433: 

434: 

435: \item[{\textbf{\em Certifier.}}]

436: Together, Equations (\ref{eq:1}) and (\ref{ecuacion2}) define a certifier

437: which provides program fixpoints, $ \p_\alpha$, as certificates which

438: entail a given safety policy, i.e., by taking $\cert = \p_\alpha$.

439: 

440: \medskip

441: 

442: \item[\textbf{\em Checking.}]

443:   A checker is a function {\sc

444:     Checker}$:{\it Prog} \times \adom \times \acert \mapsto bool$

445:   which for a program $P \in {\it Prog}$, an abstract domain $\dom \in

446:     \adom$ and

447:   certificate $\cert \in \acert$ checks

448: whether $\cert$ is a fixpoint of $S^{\alpha}_P$ or not:

449: 

450: \begin{equation}\label{eq:3}

451: \small\mbox{{\sc checker}}(P,\dom,\cert) \ {\it returns\  true\ iff}\  (S^{\alpha}_P(\cert) \equiv \cert)

452: \end{equation}

453: 

454: \medskip

455: 

456: \item[\textbf{\em Verification Condition Regeneration.}] To retain the safety

457: guarantees, the consumer must regenerate a trustworthy verification

458: condition --Equation (\ref{ecuacion2})-- and use the incoming

459: certificate to test for adherence of the safety policy.

460: 

461: 

462: \begin{equation}\label{eq:4}

463: {\it  P \ is \ trusted\ iff}\  \cert \sqsubseteq \inten

464: \end{equation}

465: 

466: \noindent

467: A fundamental idea in ACC is that, while analysis --Equation

468: (\ref{eq:1})-- is an iterative process, checking --Equation~(\ref{eq:3})-- is guaranteed to be

469: done in a \emph{single pass} over the abstraction.

470: 

471: 

472: \end{description}

473: 

474: \section{A General View of Incremental ACC}

475: \label{sec:incremental-acc}

476: 

477: 

478: Figures~\ref{inc-acc1} and \ref{inc-acc2} present a general view of

479: the incremental certification and incremental checking processes

480: respectively. In Figure \ref{inc-acc1}, the producer starts from an

481: {\sf Updated Program}, $\eprog$, w.r.t.\ a previously certified {\sf

482:   Program}, $P$.  It first retrieves from disk $P$ and its

483: certificate, \certificateA, computed in the previous certification

484: phase.  Next, the process ``$\ominus$'' compares both programs and

485: returns the differences between them, $\Mod{P}$, i.e, the program {\sf

486:   Updates} which applied to $P$ results in $\eprog$, written as

487: $\Mod{P}=\eprog \ominus P$.  Note that, from an implementation

488: perspective, a program update should contain both the new updates to

489: be applied to the program and instructions on where to place and

490: remove such new code. This can be easily done by using the traditional

491: Unix \emph{diff} format for coding program updates. An {\sf

492:   Incremental Certifier} generates from \certificateA, $P$ and

493: $\Mod{P}$ an incremental certificate, \certificateB, which can be used

494: by the consumer to validate the new updates. The package

495: ``$\Mod{P}$+\certificateB'' is submitted to the code consumer.

496: Finally, in order to have a compositional incremental approach, the

497: producer has to update the original certificate and program with the

498: new updates.

499: Thus, the resulting \certificateL\ and $\eprog$ are stored in disk

500: replacing \certificateA\ and $P$, respectively.

501: 

502: 

503: 

504: 

505: \begin{figure*}

506: \begin{center}

507: \rotatebox{-90}{

508: \scalebox{.53}{\includegraphics{inc-acc1}}}

509: \end{center}

510: \caption{Incremental Certification in  Abstraction-Carrying Code}

511: \label{inc-acc1}

512: \end{figure*}

513: 

514: 

515: \noindent

516: In Figure \ref{inc-acc2}, the consumer receives the untrusted

517: package. In order to validate the incoming update w.r.t.\ the provided

518: (incremental) certificate, it first retrieves  $P$ and

519: \certificateA~from disk. Next, it reconstructs the updated program by using an

520: operator ``$\odot$'' which applies the update to $P$ and generates

521: $\eprog=P\odot\Mod{P}$. This can implemented by using a program in the

522: spirit of the traditional Unix \emph{patch} command as $\odot$

523: operator.  An {\sf Incremental Checker} now efficiently validates the

524: new modification by using the stored data and the incoming incremental

525: certificate. If the validation succeeds (returns {\sf ok}), the

526: checker will have reconstructed the full certificate.  As before, the

527: updated program and extended certificate are stored in disk

528: (superseding the previous versions) for future (incremental) updates.

529: In order to simplify our scheme, we assume that the safety policy and

530: the generation of the verification condition \cite{Nec97} are embedded

531: within the certifier and checker. However, in an incremental approach,

532: producer and consumer could perfectly agree on a new safety policy to

533: be implied by the modification. It should be noted that this does not

534: affect our incremental approach and the verification condition would

535: be generated exactly as in non incremental PCC.

536: 

537: 

538: \begin{figure*}

539: \begin{center}

540: \rotatebox{-90}{

541: \scalebox{.53}{\includegraphics{inc-acc2}}}

542: \end{center}

543: \caption{Incremental Checking in Abstraction-Carrying Code}

544: \label{inc-acc2}

545: \end{figure*}

546: 

547: 

548: 

549: \section{Characterization of Updates}

550: \label{cu}

551: 

552: Let us now characterize the types of updates we consider and how they

553: can be dealt within the ACC scheme in the context of logic

554: programming.  

555: Given a program $P$, we define an

556: \emph{update} of $P$, written as $\Mod{P}$, as a set of tuples of the

557: form $\langle A,\addition{A},\deletion{A} \rangle$, where

558: $A=p(x_1,\ldots,x_n)$ is an atom in base form  and:

559: 

560: \begin{itemize}

561: \item $\addition{A}$ is the set of rules which are to be added to $P$

562:   for predicate $p$.  This includes both the case of addition of new

563:  predicates, when $p$ did not exist in $P$, as well as the extension

564:   of additional rules (or functionality) for $p$, if it existed.

565: 

566: 

567: \item $\deletion{A}$ is the set of rules which are to be removed from

568:   $P$ for predicate $p$.

569: \end{itemize}

570: 

571: \noindent

572: Note that, for the sake of simplicity, we do not include the

573: instructions on where to place and remove such code in the

574: formalization of our method. We distinguish three classes of updates:

575: {\em addition}, {\em deletion} and {\em arbitrary changes}.

576: 

577: \begin{itemize}

578: \item The addition of predicates occurs when $\forall A,$  $\deletion{A}

579: = \emptyset \ \wedge \ \exists A, \ \addition{A} \not = \emptyset$. 

580: 

581: \item The \emph{deletion} of predicates occurs if $\forall A,$ $

582: \addition{A} = \emptyset\ \wedge \ \exists A, \ \deletion{A} 

583: \not = \emptyset$. 

584: 

585: \item The remaining cases are considered

586: \emph{arbitrary changes}.

587: 

588: \end{itemize}

589: 

590: 

591: 

592: \medskip

593: 

594: \begin{description}

595: \item[{\textbf{\em Addition of Procedures.}}]

596: When a program $P$ is extended with new predicates or new clauses for

597: existing predicates, the original certificate $\cert$ is not

598: guaranteed to be a fixpoint any longer, because the contribution of

599: the new rules can lead to a more general answer. Consider $P^{add}$

600: the program after applying some additions and $\certadd$ the

601: certificate computed from scratch for $P^{add}$. Then, $\cert

602: \sqsubseteq \certadd$. This means that $\cert$ is no longer valid.

603: Therefore, we need to perform the least upper bound (\emph{lub}) of

604: the contribution of the new rules and submit, together with the

605: extension, the new certificate $\certadd$ (or the difference of both

606: certificates). The consumer will thus test the safety policy w.r.t.\

607: $\certadd$. Consider the abstract operation ${\sf

608:   Alub}(\CP{}_1,\CP{}_2)$ which performs the abstract disjunction of

609: two descriptions. Then, we define $\certadd = {\sf

610:   Alub}(\cert,\sqbrack{P^{add}}_\alpha)$ and submit the incremental

611: certificate $\certificateA$ which is defined as the (abstract)

612: difference $\certadd - \cert$.  The notion of incremental certificate

613: is the issue of Section~\ref{icertificates}.

614: 

615: 

616: 

617: \medskip

618: 

619: \item[{\textbf{\em Deletion of Procedures.}}]

620: The first thing to note is that in order to entail the safety policy,

621: unlike extensions over the program, we need not change the certificate

622: at all when some predicates are deleted. Consider $P^{del}$ the

623: program after applying some deletions and $\certdel$ the certificate

624: computed from scratch for $P^{del}$.  The original certificate $\cert$

625: is trivially guaranteed to be a fixpoint (hence a correct

626: certificate), because the contribution of the rules was conjoined (by

627: computing the lub) to give $\cert$ and so it still correctly describes

628: the contribution of each remaining rule.  By applying

629: Equation~\ref{ecuacion2}, $\cert$ is still valid for $P^{del}$ w.r.t.

630: $\inten$ since $ \cert \sqsubseteq \inten$.

631: Therefore, more accuracy is not needed to ensure compliance with the

632: safety policy. This suggests that the incremental certificate can be

633: empty and the checking process does not have to check any predicate.

634: However, it can happen that a new, more precise, safety policy is

635: agreed by the consumer and producer. Also, this accuracy could be

636: required in a later modification. Although $\cert$ is a correct

637: certificate, it is possibly less \emph{accurate} than $\certdel$,

638: i.e., $\certdel \sqsubseteq \cert$.  It is therefore interesting to

639: define the corresponding incremental algorithm for reconstructing

640: $\certdel$ and checking the deletions and the propagation of their

641: effects.

642: 

643: \medskip

644: 

645: 

646: \item[\textbf{\em Arbitrary Changes.}]  The case of arbitrary changes

647: considers that rules can both be deleted from and added to an already

648: validated program. In this case, the new certificate for the modified

649: program can be either equal, more or less precise than the original

650: one, or even not comparable.  

651: Imagine that an arbitrary change replaces a rule

652: $R_a$, which contributes to a fixpoint $\cert^{a}$, with a new one

653: $R_b$ which contributes to a fixpoint $\cert^{b}$ such that

654: $\cert^{ab} = \alub(\cert^{a} , \cert^{b})$ and $\cert^{a} \sqsubset

655: \cert^{ab}$ and $\cert^{b} \sqsubset \cert^{ab}$. 

656: The point is that we cannot just compute an approximation of the new

657: rule and compute the lub with to the previous fixpoint, i.e., we

658: cannot use $\cert^{ab}$ as certificate and have to provide the more

659: accurate $\cert^{b}$.  The reason is that it might be possible to

660: attest the safety policy by independently using $\cert^{a}$ and

661: $\cert^{b}$ while it cannot be implied by using their lub

662: $\cert^{ab}$. This happens for certain safety policies which contain

663: disjunctions, i.e., $\cert^{a} \vee \cert^{b}$ does not correspond to

664: their lub $\cert^{ab}$.  Therefore, arbitrary changes require a

665: precise recomputation of the new fixpoint and its proper checking.

666: 

667: As a practical remark, an arbitrary update can be decomposed into an

668: addition and a deletion and then handled as the first cases. We have

669: pointed out the difference because correctness and accuracy

670: requirements are different in each particular case, as we have

671: seen above.

672: 

673: \end{description}

674: 

675: \begin{example} \label{programas}

676:  The next example shows a piece of a module which contains the

677:   following (normalized) program for the naive reversal of a list and

678:   uses the standard implementation of {\tt app} for appending lists:

679: 

680: 

681: 

682: \[\begin{array}{lll}

683: P_0 \equiv & \left\{

684: \begin{array}{lll}

685: ({\tt rev_1}) & {\tt rev(X,Y)   :- ~X = [\ ],~ Y = [\ ].} \\

686: ({\tt rev_2}) & {\tt rev(X,Y)   :- ~X = [U|V],~ rev(V, W),~ T = [U],~

687:   app(W, T, Y).} \\

688: ({\tt app_1})&{\tt app(X,Y,Z) :-~ X = [\ ],~ Y = Z.} \\

689: ({\tt app_4})& {\tt app(X,Y,Z) :-~ X = [U|V],~ Z = [U|W],~ app(V,Y,W)}.

690: \end{array}\right.

691: \end{array}\]

692: 

693: 

694: 

695: \noindent

696: Suppose now that the consumer modifies $P_0$ introducing two more base cases

697: for $\tt app$ (e.g., added automatically by a partial evaluator

698: \cite{pevalbook93}):

699: 

700: 

701: 

702: \[\begin{array}{lll}

703: ({\tt app_2}) &{\tt app(X,Y,Z) :-~ X = [U],~ Z = [U|Y].} \\

704: ({\tt app_3}) &{\tt app(X,Y,Z) :-~ X = [U,V],~ Z = [U,V|Y].}

705: \end{array}\]

706: 

707: 

708: 

709: \noindent

710: The producer must send to the consumer the set  $\Mod{P_0}$,

711: composed of the unique tuple:

712: 

713: \[\langle {\tt app(X,Y,Z)}, {\it Add}({\tt

714:   app(X,Y,Z)}), {\it Del}({\tt app(X,Y,Z)}) \rangle\]

715: 

716: \noindent

717: where $\addition{{\tt app(X,Y,Z)}} = \{{\tt app_2},{\tt app_3}\}$ and

718: $\deletion{{\tt app(X,Y,Z)}} = \emptyset$, i.e., we are in the case of

719: an {\em addition} of predicates only. Let us name $P_1$ to the program

720: resulting from adding rules ${\tt app_2}$ and ${\tt app_3}$ to $P_0$.

721: Note that these rules do not add any further information to the

722: program (i.e., the certificate for $P_0$ and $P_1$ would remain the

723: same and, as we will see, the {\em incremental certificate is empty}).

724: 

725: 

726: Consider now the following new definition

727: for predicate {\tt app} which is a specialization of the previous

728:   {\tt app} to concatenate lists of {\tt a}'s of the same length:

729: 

730: 

731: 

732: \[\begin{array}{lll}

733: {\tt (Napp_1)} &{\tt app(X,Y,Z) :-~ X = [\ ],Y = [\ ], Z = [\ ].}\\

734: {\tt (Napp_2)} & {\tt app(X,Y,Z) :-~ X = [a|V],Y=[a|U], Z = [a,a|W],

735:      app(V,U,W)}.

736: \end{array}\]

737: 

738: 

739: 

740: 

741: \noindent

742: The update consists in deleting all rules for predicate {\tt app} in

743: $P_1$ and replacing them by ${\tt Napp_1}$ and

744: ${\tt Napp_2}$. Let $P_2$ be the resulting program.

745: $\Mod{P_1}$ is composed again of a unique tuple with

746: the following information:

747: 

748: 

749: 

750: \[ \begin{array}{lll}

751: \addition{{\tt app(X,Y,Z)}}=\{{\tt Napp_1}, {\tt Napp_2}\}\\

752: \deletion{{\tt app(X,Y,Z)}}= {\tt \{app_1,app_2,app_3,app_4\}}

753: \end{array} \]

754: 

755: 

756: 

757: \noindent

758: In this case, we are in presence of an {\em arbitrary change}, and as

759: we will show in Example \ref{ultimo}, the {\em incremental

760:   certificate} will not be empty in this case (since by using the

761: abstract domain  $\defff$ in Example \ref{ex:dom-call}, the

762: fixpoint for $P_2$ will change w.r.t. the one for $P_1$).  \hfill

763: $\Box$

764: \end{example}

765: 

766: \section{Incremental Certificates}

767: \label{icertificates}

768: 

769: 

770: Although ACC and incremental ACC, as outlined above, are general

771: proposals not tied to any particular programming paradigm, our

772: developments for incremental ACC (as well as for the original ACC

773: framework \cite{lpar04-ai-safety}) are formalized in the context of

774: (C)LP. A main idea in ACC \cite{lpar04-ai-safety} is that a {\em

775:   certificate}, $\certificateA$, is automatically generated by using

776: the \emph{complete} set of {\em entries} returned by an abstract

777: fixpoint analysis algorithm. For concreteness, we rely on an abstract

778: interpretation-based analysis algorithm in the style of the generic

779: analyzer of \cite{incanal-toplas}. 

780: 

781: The analysis algorithm of \cite{incanal-toplas}, which we refer to as

782: \analyzerA, given a program $P$ and an abstract domain

783: $\dom$, receives a set of {\em

784:   call patterns} $\atom \in \aatom$ (or Abstract Atoms)

785:    which are a description of

786: the calling modes into the program, and constructs an \emph{analysis

787:   graph}~\cite{bruy91} for $\atom$ which is an \emph{abstraction} of

788: the (possibly infinite) set of (possibly infinite) trees explored by

789: the concrete execution of initial calls described by $\atom$ in $P$.

790: Formally, a \emph{call pattern} $A:{\it CP} \in \aatom$ is composed of an atom in

791: base form, $A \equiv p(X_1,\ldots, X_n)$, and a description

792: in the abstract domain, ${\it CP}$, for $A$.

793: 

794: 

795: The program analysis graph computed by \analyzerA$(\atom)$ for $P$ in

796: $\dom$ can be implicitly represented by means of two data structures,

797: the {\em answer table} (${\it AT}$) and the {\em dependency arc table}

798: (${\it DAT}$), which are the

799: output of the algorithm  \analyzerA.

800: Each element (or {\em entry})

801: in the answer table takes the form $A:{\it CP} \mapsto {\it AP}$ such

802: that, for the atom $A$, ${\it CP}$ is its \emph{call} description and

803: ${\it AP}$ its \emph{success} (or answer) description in the abstract

804: domain. Informally, such entry should be interpreted as ``the answer

805: pattern for calls to $A$ satisfying precondition ${\it CP}$ accomplishes

806: postcondition $AP$''.  The

807: dependency arc table is not relevant now, although it is

808: fundamental in the design of the incremental checking, as we will see

809: later.  All the details and the formalization of the algorithm can be

810: found in \cite{incanal-toplas}.

811: 

812: 

813: 

814: 

815: 

816: 

817: 

818: 

819: 

820: 

821: Our proposal for the incremental checking is that,

822: if the consumer keeps the original (fixed-point)

823: abstraction $\certificateA$, it is possible to provide only the

824: program updates and

825: the incremental certificate $\certificateB$. Concretely, given:

826: 

827: \begin{itemize}

828: \item an update $\Mod{P}$ of $P$,

829: \item the certificate \certificateA~for

830: $P$ and $\atom$,

831: \item the certificate \certificateL~for

832: $P\odot\Mod{P}$ and $\atom$

833: \end{itemize}

834: 

835: \noindent

836: we define \certificateB, the

837: \emph{incremental certificate} for $\Mod{P}$ w.r.t.\ $\certificateA$,

838: as the difference of certificates $\certificateL$ and $\certificateA$,

839: i.e., the set of entries in $\certificateL$ not occurring in $\certificateA$.

840: The first obvious advantage is that the size of the

841: transmitted certificate can be considerably reduced.  Let us see an example.

842: 

843: 

844: 

845: \begin{example}\label{ex:dom-call} Consider program $P_0$ in Example

846:   \ref{programas}. The description domain that we are going to use in our examples

847:   is the {\em

848:     definite Boolean functions}~\cite{pos-def94}, denoted $\defff$.

849:   The key idea in this description is to use implication to capture

850:   groundness dependencies.  The reading of the function $x \rightarrow

851:   y$ is ``if the program variable $x$ is (becomes) ground, so is

852:   (does) program variable $y$.''  For example, the best description of

853:   the constraint ${\tt f(X,Y) = f(a,g(U,V))}$ is ${\tt X \wedge (Y

854:   \leftrightarrow (U \wedge V))}$.

855:   The most general description $\tt \top$ does not provide information

856:   about any variable.  The least general substitution $\tt \bot$

857:   assigns the empty set of values to each variable.

858: For the analysis of our running example, we consider the set of

859:  call

860:   patterns $\atom=\{{\tt rev(X,}$ ${\tt Y):\top}\}$, i.e., no entry information

861:   is provided on $\tt X$ nor $\tt Y$. \analyzerA(\{${\tt rev(X,

862:     Y):\top}$\})~returns in the answer table, ${\it AT}$, the following entries:

863: 

864: 

865: \[ \begin{array}{ll@{~~~~~~}llllll}

866: ({\it A_1})& \ \ \entry{\tt rev(X, Y) : \top }{ \tt X \leftrightarrow

867:   Y}  \\

868: ({\it A_2})& \ \ \entry{\tt app(X, Y, Z) : \top}{\tt  (X \wedge Y)

869:   \leftrightarrow Z}

870: \end{array} \]

871: 

872: 

873: 

874: 

875: 

876: \noindent

877: The certificate

878: \certificateA~for this example is then composed of the entries ${\it

879:   A_1}$ and ${\it A_2}$.

880: Consider now the addition of rules $\tt app_2$ and $\tt app_3$ in

881: $P_0$, i.e., program $P_1$ of Example \ref{programas}.

882: The analysis algorithm of \cite{incanal-toplas}

883: returns as $\certificateL$ the same answer table ${\it AT}$ as for

884: $P_0$, since the added

885: rules do

886: not affect the fixpoint result, i.e., they do not add any further

887: information. Thus, the incremental certificate

888: \certificateB~associated to such an update is empty.  \hfill $\Box$

889: 

890: \end{example}

891: 

892: 

893: \section{Incremental Checking}

894: \label{icheckers}

895: Intuitively, an  abstract interpretation-based checking algorithm

896: (like the one in \cite{lpar04-ai-safety})

897: receives as input a program $P$, a set of abstract atoms $\atom$ and a

898: certificate \certificateA\, and constructs a program analysis graph in

899: a single iteration by assuming the fixpoint information in

900: \certificateA.

901: While the graph is being constructed,

902: the obtained answers are stored in an answer table ${\it AT_{\it

903:     mem}}$ (initially empty)

904: and compared with the corresponding fixpoints stored in \certificateA.

905: If any of the computed answers is not consistent with the certificate

906: (i.e., it is greater than the fixpoint), the certificate is considered

907: invalid and the program is rejected.

908: Otherwise, \certificateA~gets accepted 

909: and ${\it AT_{\it mem}} \equiv \certificateA$.

910: 

911:  \subsection{Checking with Dependencies}

912: 

913:  In order to define an incremental checking, the checking algorithm in

914:  \cite{lpar04-ai-safety} needs to be modified to compute (and store)

915:  also the dependencies between the atoms in the answer table.  In

916:  \cite{inc-acc-tr}, we have instrumented a checking algorithm for full

917:  certificates with a \emph{Dependency Arc Table}.  This structure, ${\it DAT}$, is not required by non

918:  incremental checkers but it is fundamental to support an incremental

919:  design.

920: The ${\it DAT}$ returned by \analyzerA~is composed of

921:  arcs (or {\em dependencies}) of the form $A_k:{\it CP} \Rightarrow

922:  B_{k,i}:{\it CP}'$ associated to a program rule $A_k \mbox{ :- }

923:  B_{k,1},\ldots,B_{k,n}$ with $i \in \{1,..n\}$, where $ B_{k,i}$ is an atom.  The intended meaning

924:  of such a dependency is that the answer for $A_k:{\it CP}$ depends on the

925:  answer for $B_{k,i}:{\it CP}'$, say ${\it AP}$.  Thus, if ${\it AP}$ changes with

926:  the update of some rule for $B_{k,i}$ then, the arc $A_k:{\it CP}

927:  \Rightarrow \ B_{k,i}:{\it CP}'$ must be reprocessed in order to compute

928:  the new answer for $A_k:{\it CP}$. This is to say that the rule for $A_k$

929:  has to be processed again starting from atom $B_{k,i}$, i.e., we do

930:  not need to process the part  $A_k \mbox{ :- }

931:  B_{k,1},\ldots,B_{k,i-1}$ because it is not affected by the changes.

932: 

933: 

934: 

935:  In the following, we assume that {\sc checker} is a non incremental

936:  checker such that, if the call {\sc checker}($P,\atom,\certificateA$)

937:  does not fail, then it returns the reconstructed answer table ${\it

938:    AT_{\it mem}}$ and the set of dependencies ${\it DAT_{\it mem}}$

939:  which have been generated. In such a case, we say that $\certificateA$

940:  has been {\em checked} or {\em accepted}. By the correctness of the checker

941:  \cite{lpar04-ai-safety}, the reconstructed structures contain exactly

942:  the same data as the answer table and the dependency arc table

943:  computed by the analysis algorithm \analyzerA($\atom$) for the

944:  program $P$.

945: 

946: 

947: 

948: 

949: 

950: 

951: 

952: \begin{example}\label{ex:dom-call1} Consider the program $P_0$ in

953:   Example \ref{programas}. \analyzerA~returns, together with ${\it

954:     AT}$, the following dependency arc table:

955: 

956: 

957: 

958: \[ \begin{array}{llllllll}

959:  ({\it D_1}) & \dependency{\tt rev(X,Y):\top}{\tt rev(V,W):\top} \\

960:  ({\it D_2}) & \dependency{\tt

961:   rev(X,Y):\top}{\tt app(W,T,Y):\top} \\

962: ({\it D_3}) & \dependency{\tt app(X,Y,Z):\top}{\tt app(V,Y,W):\top}

963: \end{array} \]

964: 

965: 

966: 

967: 

968: \noindent

969: Intuitively, $D_2$ denotes that the answer for ${\tt rev(X,Y):\top}$

970: may change if the answer for ${\tt app(W,T,Y):\top}$ changes. In such

971: a case, the second rule $\tt rev_2$ for ${\tt rev}$ must be processed

972: again starting from atom ${\tt app(W,T,Y)}$ in order to recompute the

973: fixpoint for ${\tt rev(X,Y):\top}$.  $D_1$ and $D_3$ reflect the

974: recursivity of ${\tt rev(X,Y):\top}$ and ${\tt app(W,}$ ${\tt

975:   T,Y):\top}$, respectively, since they depend on themselves (rules

976: $\tt rev_2$ and $\tt app_4$ respectively).  The detailed steps

977: performed by the algorithm can be found in \cite{incanal-toplas}. Note

978: that, the {\sc checker} executed for the call pattern at hand,

979: computes (and stores) in ${\it AT_{\it mem}}$ the entries $A_1$, $A_2$

980: in Example \ref{ex:dom-call}, and, after traversing rules $\tt rev_2$

981: and $\tt app_4$, it stores in ${\it DAT_{\it mem}}$ the dependencies

982: $D_1$, $D_2$ and $D_3$.  \hfill $\Box$

983: 

984: \end{example}

985: 

986: 

987: \subsection{Additional Tasks of an Incremental Checker}

988: \noindent

989: In order to support incrementality, the final values of the data

990: structures ${\it AT_{\it mem}}$, ${\it DAT_{\it mem}}$ and $P$ must be

991: available after the end of the execution of the checker. Thus, we

992: denote by ${\it AT_{\it persist}}$, ${\it DAT_{\it persist}}$ and

993: ${\it P}_{persist}$ the copy in persistent memory (i.e., in disk) of

994: such structures. Now, we outline in a very general way the additional

995: tasks that  an incremental checking algorithm

996: ({\sc inc\_check} in the following) has to perform. The complete code

997: of the algorithm can be found in \cite{inc-acc-tr}.

998: It receives as input

999: parameters an update $\Mod{P}$ of the original program $P$, a set of

1000: abstract atoms  $\atom \in \aatom$ and the incremental certificate

1001: $\certificateB$ for $\Mod{P}$ w.r.t. $\certificateA$. The following

1002: tasks are carried out by an incremental checker:

1003: 

1004: 

1005: \begin{description}

1006: 

1007: \item[{\bf Step 1)}] It retrieves from memory ${\it AT_{mem}}:={\it AT_{persist}}$,

1008:   ${\it DAT}_{\it mem}$ $:={\it DAT}_{\it persist}$ and $P:=

1009:   P_{persist}$ (stored in persistent memory in a previous checking

1010:   phase) and generates $P_{\it mem}:=P \odot \Mod{P}$.

1011: 

1012: \medskip

1013: 

1014: \item[{\bf Step 2)}] It rechecks all entries in

1015: ${\it AT_{mem}}$ which have been directly affected by an

1016: update. Concretely, for each $A:{\it CP} \in {\it AT_{mem}}$, such

1017: that $A$ has an entry in $\Mod{P}$, a call to {\sc checker}$(P \odot

1018: \Mod{P}, \{A:{\it CP}\}, \certificateB)$ is generated, marking the

1019: entry as {\em checked} (or {\em accepted}) $A:{\it

1020:   CP}^{\it check}$. This guarantees that the incremental checking

1021: process is done in one pass (i.e., rules used to check $A:{\it CP}$

1022: are traversed at most once).

1023: 

1024: \medskip

1025: 

1026: \item [{\bf Step 3)}] It propagates and rechecks the indirect effect of these

1027:   changes by inspecting the dependencies in ${\it DAT_{\it mem}}$.

1028:   Thus, for all $A:{\it CP}^{check} \in \certificateB$, if there

1029:   exists a dependency of the form $B:{\it CP_B} \Rightarrow A:{\it

1030:     CP}$ (modulo renaming) in ${\it DAT_{\it mem}}$ such that $B:{\it

1031:     CP_B}$ is not marked as checked, then a call to {\sc checker}$(P

1032:   \odot \Mod{P}, \{B:{\it CP_B}\}, \certificateB)$ is generated and

1033:   $B:{\it CP}_B$ is marked as checked. This process is repeated until

1034:   there are no dependencies satisfying the above condition. Note

1035:   that the condition $A:{\it CP}^{check} \in \certificateB$ ensures

1036:   that the answer for $A:{\it CP}$ has changed w.r.t. $\certificateA$.

1037:   Otherwise nothing has to be done (this will allow us to reduce the

1038:   checking time w.r.t a full checking process for $P$ and

1039:   $\certificateL$).

1040: 

1041: \medskip

1042: 

1043: \item[{\bf Step 4)}]  If it does not issue an \error~then it removes

1044: from ${\it AT}_{\it mem}$ those entries

1045: corresponding to deleted rules. We can identity them by exploring

1046: ${\it DAT_{\it mem}}$. Concretely, for all $A:{\it CP} \in {\it

1047:   AT}_{\it mem}$, $A:{\it CP} \not \in S_{\it \alpha}$, if

1048: there not exists a dependency $B:{\it CP'} \Rightarrow A:{\it CP}$ in

1049: ${\it DAT_{\it mem}}$ then remove $A:{\it CP}$ from ${\it AT_{\it

1050:     mem}}$.

1051: 

1052: \medskip

1053: 

1054: \item[{\bf Step 5)}] It stores

1055:  ${\it AT_{\it persist}}:={\it AT_{\it

1056:       mem}}$,  ${\it DAT_{\it persist}}$ $:={\it DAT_{\it mem}}$ and

1057: ${\it P_{\it persist}}:=P_{\it mem}$.

1058: 

1059: 

1060: \end{description}

1061: %

1062: Our first example is intended to illustrate a situation in which the

1063: task performed by the incremental checker can be optimized such that it

1064: only checks a part of the analysis graph.

1065: 

1066: 

1067: 

1068: \begin{example} \label{exampleCh1}

1069: Consider the addition of rules $\tt app_2$ and $\tt app_3$ to program

1070: $P_0$, which results in program $P_1$ (Example

1071: \ref{programas}). As shown in Example \ref{ex:dom-call},

1072: the incremental certificate

1073: \certificateB~associated to such an update is empty.

1074: The incremental checking

1075: algorithm {\sc inc\_check} proceeds as follows:

1076: 

1077: \begin{description}

1078: \item[{\bf Step 1)}]  ${\it AT}_{\it mem}$ and

1079: ${\it DAT}_{\it mem}$ are initialized with $A_1$,$A_2$ (Example

1080: \ref{ex:dom-call})  and $D_1$,$D_2$

1081: and $D_3$ (Example \ref{ex:dom-call1}) respectively.

1082: $P_{\it mem} \equiv P_1$.

1083: 

1084: \medskip

1085: 

1086: \item[{\bf Step 2)}] Since ${\tt

1087:   app(X,Y,Z):\top}

1088: \in {\it AT_{\it mem}}$ and $\addition{{\tt app(X,Y,Z)}}$ is not empty, then

1089: a call to {\sc checker}($P_1$,\{$\tt app(X,Y,Z):\top$\},$\certificateB$)

1090: is generated

1091:  in order to ensure that the fixpoint is preserved. Now, $\tt

1092:  app(X,Y,Z):\top$ is marked as checked.

1093: 

1094: 

1095: \medskip

1096: 

1097: \item[{\bf Step 3)}] No checking has to be done since $\certificateB$

1098:   is empty.

1099: 

1100: \medskip

1101: 

1102: \item[{\bf Step 4)}] Nothing is done since $\tt app(X,Y,Z):\top$

1103:   occurs at the right-hand side of dependency $D_3$.

1104: 

1105: \medskip

1106: 

1107: \item[{\bf Step 5)}] Finally,

1108: once \certificateB~has been validated, the

1109: consumer stores the answer table ${\it AT_{\it mem}}$, the dependency

1110: arc table ${\it DAT_{\it mem}}$ and

1111: the program $P_{\it mem}$ in disk with the same values as in

1112: Step 1. \hfill $\Box$

1113: \end{description}

1114: \end{example}

1115: 

1116: \noindent

1117: Our second example is intended to show how to propagate the effect of

1118: a change to the part of the analysis graph indirectly affected by such update.

1119: 

1120: 

1121: 

1122: \begin{example} \label{ultimo}

1123: The update consists in deleting all rules for predicate {\tt app} in

1124: program $P_1$ of Example~\ref{programas} (which results in program

1125: $P_2$),  and replacing them

1126: by ${\tt Napp_1}$ and

1127: ${\tt Napp_2}$. After running the \analyzerA~for $P_2$,

1128: the following answer table and dependencies are computed:

1129: 

1130: 

1131: 

1132: \[ \begin{array}{llllllll}

1133: {\it (NA_1)}\ \ \entry{\tt rev(X, Y) : \top}{\tt X \wedge Y}  \\

1134: {\it (NA_2)}\ \ \entry{\tt app(X, Y,Z) : \top}{\tt X \wedge Y \wedge Z}\\

1135: {\it (NA_3)}\ \ \entry{\tt app(X, Y,Z) : X}{\tt X \wedge Y \wedge Z} \\

1136: {\it (ND_1)}\ \ \dependency{\tt rev(X,Y):\top}{\tt rev(V,W):\top} \\

1137: {\it (ND_2)}\ \   \dependency{\tt rev(X,Y):\top}{\tt app(W,T,Y):W} \\

1138: {\it (ND_3)}\ \  \dependency{\tt app(X,Y,Z):X}{\tt app(V,U,W):V}

1139: \end{array} \]

1140: 

1141: 

1142: 

1143: \noindent

1144: Note that the

1145: analysis information has changed because the new

1146: definition of {\tt app} allows inferring that all its arguments are

1147: ground upon success ${\it (NA_2}$ and ${\it NA_3)}$.\footnote{Note hat

1148: ${\it NA_3}$ is subsumed by ${\it NA_2}$ and we could indeed only

1149: submit  ${\it NA_2}$. The incremental checking algorithm should be

1150: modified to search entries which are equal or more general than the

1151: required one.} This change

1152: propagates to the answer of {\tt rev} and allows inferring that,

1153: regardless of the call pattern, both arguments of {\tt rev} will be

1154: ground on the exit ${\it (NA_1)}$. The incremental

1155: certificate \certificateB~contains ${\it NA_3}$ as it corresponds to a

1156: new call pattern and contains also ${\it NA_1}$ and

1157: ${\it NA_2}$ since their answers have changed w.r.t. the ones stored in

1158: $\certificateA$ (Example~\ref{ex:dom-call}).

1159: Let us illustrate the incremental checking process carried out to

1160: validate this update.

1161: 

1162: \begin{description}

1163: \item[{\bf Step 1)}] We retrieve

1164: from disk the answer table, dependency arc table and the program

1165: stored in Step 5 of Example \ref{exampleCh1}. Now $P_{\it mem} \equiv P_2$.

1166: 

1167: \medskip

1168: 

1169: \item[{\bf Step 2)}] Similar to Step 2 of Example  \ref{exampleCh1},

1170:   but considering the new rules for $\tt app$.

1171: 

1172: \medskip

1173: 

1174: \item[{\bf Step 3)}] Since we have the dependency $D_2 \in {\it DAT_{\it mem}}$ and

1175: ${\tt app(X,Y,Z):\top} \in \certificateB$,

1176: a call to {\sc checker}($P_2$,$\{\tt rev(X,Y):\top\}$,$\certificateB$) is

1177: generated to ensure that the new fixpoint for $\tt rev(X,Y):\top$ is

1178: valid. In the checking process, when traversing the rule $\tt rev_2$,

1179: the new call pattern $\tt app(X,Y,Z):X$ occurs and it is also

1180: validated by calling to {\sc checker}. When traversing rule $\tt

1181: Napp_2$, the dependency $D_3$ is replaced by the new one ${\it ND_3}$

1182: in ${\it DAT_{\it mem}}$, and the call pattern is marked as checked.

1183: Similarly, the

1184: dependency ${\it D_2}$ is replaced by

1185: the new one ${\it ND_2}$ and

1186:  $\tt rev(X,Y):\top$

1187: is marked as checked. Now, all call patterns have been checked and the

1188: process finishes.

1189: 

1190: \medskip

1191: 

1192: \item[{\bf Step 4)}] The entry ${\it NA}_2$ is removed from ${\it

1193:     AT_{\it mem}}$ since it does not occur at the right-hand side of

1194:   any dependency.

1195: 

1196: \medskip

1197: 

1198: \item[{\bf Step 5)}] The

1199: consumer stores the answer table ${\it AT_{\it mem}}:=\{{\it

1200:   NA_1,NA_3}\}$,

1201: the dependency

1202: arc table ${\it DAT_{\it mem}}:=\{{\it ND_1,ND_2,ND_3}\}$ and

1203: the program $P_{\it mem} := P_2$ in disk. \hfill $\Box$

1204: 

1205: 

1206: \end{description}

1207: \end{example}

1208: The definition of the algorithm {\sc inc\_check} can be found in

1209: \cite{inc-acc-tr}, together with the proof of the correctness of the

1210: algorithm. Informally, correctness amounts to saying that if {\sc

1211:   inc\_check} does not issue an error, then it returns as computed

1212: answer table the extended certificate $\certificateL$ for the updated

1213: program.  Moreover, we ensure that it does not iterate during the

1214: reconstruction of any answer.

1215: 

1216: \section{Conclusions}\label{sec:discussion}

1217: 

1218: 

1219: 

1220: 

1221: Our proposal to incremental ACC aims at reducing the size of

1222: certificates and the checking time when a supplier provides an

1223: untrusted update of a (previously) validated package.  Essentially,

1224: when a program is subject to an update, the incremental certificate we

1225: propose contains only the \emph{difference} between the original

1226: certificate for the initial program and the new certificate for the

1227: updated one.  Checking time is reduced by traversing only those parts

1228: of the abstraction which are affected by the changes rather than

1229: the whole abstraction. 

1230: An important point to note is that our incremental

1231: approach requires the original certificate and the dependency arc

1232: table to be stored by the consumer side for upcoming updates.  The

1233: appropriateness of using the incremental approach will therefore

1234: depend on the particular features of the consumer system and the

1235: frequency of software updates.  In general, our approach seems to be

1236: more suitable when the consumer prefers to minimize as much as

1237: possible the waiting time for receiving and validating the certificate

1238: while storage requirements are not scarce.  We believe that, in

1239: everyday practice, time-consuming safety tests would be avoided by

1240: many users, while they would probably accept to store the safety

1241: certificate and dependencies associated to the package. Nevertheless,

1242: there can sometimes be situations where storage resources can be very

1243: limited,

1244: while runtime resources for performing upcoming checkings could still

1245: be sufficient.

1246: %

1247: We are now in the process of extending the ACC implementation already

1248: available in the \ciaopp\ system to support incrementality. Our

1249: preliminary results in certificate reduction are very promising. 

1250: We

1251: expect optimizations in the checking time similar to those achieved in

1252: the case of incremental analysis (see, e.g., \cite{incanal-toplas}).

1253: 

1254: \section*{Acknowledgments}

1255: 

1256: 

1257: 

1258: This work was funded in part by the Information Society Technologies

1259: program of the European Commission, Future and Emerging Technologies

1260: under the IST-15905 {\em MOBIUS} project, by the Spanish Ministry of

1261: Education under the TIN-2005-09207 {\em MERIT} project, and the Madrid

1262: Regional Government under the S-0505/TIC/0407 \emph{PROMESAS} project.

1263: The authors would like to thank the anonymous referees of WLPE for

1264: their useful comments.

1265: 

1266: \bibliographystyle{plain}

1267: 

1268: \begin{thebibliography}{10}

1269: 

1270: \bibitem{inc-acc-tr}

1271: E.~Albert, P.~Arenas, and G.~Puebla.

1272: \newblock An {I}ncremental {A}pproach to {A}bstraction-{C}arrying {C}ode.

1273: \newblock Technical Report CLIP3/2006, Technical University of Madrid (UPM),

1274:   School of Computer Science, UPM, March 2006.

1275: 

1276: \bibitem{lpar04-ai-safety}

1277: E.~Albert, G.~Puebla, and M.~Hermenegildo.

1278: \newblock {A}bstraction-{Carrying} {Code}.

1279: \newblock In {\em Proc. of LPAR'04}, number 3452 in LNAI, pages 380--397.

1280:   Springer-Verlag, 2005.

1281: 

1282: \bibitem{pos-def94}

1283: T.~Armstrong, K.~Marriott, P.~Schachte, and H.~S{\o}ndergaard.

1284: \newblock Boolean functions for dependency analysis: Algebraic properties and

1285:   efficient representation.

1286: \newblock In Springer-Verlag, editor, {\em Static Analysis Symposium, SAS'94},

1287:   number 864 in LNCS, pages 266--280, Namur, Belgium, September 1994.

1288: 

1289: \bibitem{bruy91}

1290: M.~Bruynooghe.

1291: \newblock {A} {P}ractical {F}ramework for the {A}bstract {I}nterpretation of

1292:   {L}ogic {P}rograms.

1293: \newblock {\em Journal of Logic Programming}, 10:91--124, 1991.

1294: 

1295: \bibitem{Cousot77}

1296: P.~Cousot and R.~Cousot.

1297: \newblock {A}bstract {I}nterpretation: a {U}nified {L}attice {M}odel for

1298:   {S}tatic {A}nalysis of {P}rograms by {C}onstruction or {A}pproximation of

1299:   {F}ixpoints.

1300: \newblock In {\em {F}ourth {ACM} {S}ymposium on {P}rinciples of {P}rogramming

1301:   {L}anguages}, pages 238--252, 1977.

1302: 

1303: \bibitem{incanal-toplas}

1304: M.~Hermenegildo, G.~Puebla, K.~Marriott, and P.~Stuckey.

1305: \newblock {I}ncremental {A}nalysis of {C}onstraint {L}ogic {P}rograms.

1306: \newblock {\em ACM Transactions on Programming Languages and Systems},

1307:   22(2):187--223, March 2000.

1308: 

1309: \bibitem{pevalbook93}

1310: N.D. Jones, C.K. Gomard, and P.~Sestoft.

1311: \newblock {\em {P}artial {E}valuation and {A}utomatic {P}rogram {G}eneration}.

1312: \newblock Prentice Hall, New York, 1993.

1313: 

1314: \bibitem{JVM03}

1315: Xavier Leroy.

1316: \newblock Java bytecode verification: algorithms and formalizations.

1317: \newblock {\em Journal of Automated Reasoning}, 30(3-4):235--269, 2003.

1318: 

1319: \bibitem{Lloyd87}

1320: J.W. Lloyd.

1321: \newblock {\em Foundations of Logic Programming}.

1322: \newblock Springer, second, extended edition, 1987.

1323: 

1324: \bibitem{marriot-stuckey-98}

1325: Kim Marriot and Peter Stuckey.

1326: \newblock {\em {P}rogramming with {C}onstraints: {A}n {I}ntroduction}.

1327: \newblock The MIT Press, 1998.

1328: 

1329: \bibitem{Nec97}

1330: G.~{}Necula.

1331: \newblock Proof-{C}arrying {C}ode.

1332: \newblock In {\em Proc. of POPL'97}, pages 106--119. ACM Press, 1997.

1333: 

1334: \bibitem{RR98}

1335: K.~Rose, E.~Rose.

1336: \newblock Lightweight bytecode verification.

1337: \newblock In {\em OOPSLA Workshop on Formal Underpinnings of Java}, 1998.

1338: 

1339: \end{thebibliography}

1340: 

1341: 

1342: 

1343: 

1344: 

1345: 

1346: \end{document}

1347: