ABSTRACT. We consider basic symbolic heaps, i.e. symbolic heaps without any inductive predicates, but within a memory model featuring permissions. We propose a complete proof system for this logic that is entirely independent of the permission model. This is an ongoing work towards a complete proof system for symbolic heaps with lists, and more generally towards a proof theory of permissions in separation logics with recursive predicates and Boolean BI with abstract predicates.